:: Bounds in Posets and Relational Substructures
:: by Grzegorz Bancerek
::
:: Received September 10, 1996
:: Copyright (c) 1996-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, ORDERS_2, SUBSET_1, XXREAL_0, RELAT_1,
RELAT_2, REWRITE1, LATTICE3, ZFMISC_1, ORDERS_1, ARYTM_3, TARSKI,
LATTICES, XXREAL_2, EQREL_1, FILTER_0, PBOOLE, ORDINAL2, FINSET_1, CAT_1,
WELLORD1, YELLOW_0, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_2, RELSET_1, FINSET_1,
TOLER_1, ORDERS_1, DOMAIN_1, CARD_1, STRUCT_0, LATTICES, ORDERS_2,
LATTICE3;
constructors TOLER_1, REALSET2, LATTICE3;
registrations XBOOLE_0, RELSET_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3,
CARD_1;
requirements BOOLE, SUBSET, NUMERALS;
begin :: Reexamination of poset concepts
scheme :: YELLOW_0:sch 1
RelStrEx {X() -> non empty set, P[set,set]}: ex L being non empty strict
RelStr st the carrier of L = X() & for a,b being Element of L holds a <= b iff
P[a,b];
definition
let A be non empty RelStr;
redefine attr A is reflexive means
:: YELLOW_0:def 1
for x being Element of A holds x <= x;
end;
definition
let A be RelStr;
redefine attr A is transitive means
:: YELLOW_0:def 2
for x,y,z being Element of A st x <= y & y <= z holds x <= z;
redefine attr A is antisymmetric means
:: YELLOW_0:def 3
for x,y being Element of A st x <= y & y <= x holds x = y;
end;
registration
cluster complete -> with_suprema with_infima for non empty RelStr;
cluster -> complete transitive antisymmetric
for 1-element reflexive RelStr;
end;
registration
let x be set;
let R be Relation of {x};
cluster RelStr(#{x},R#) -> 1-element;
end;
registration
cluster strict 1-element reflexive for RelStr;
end;
theorem :: YELLOW_0:1
for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 for
a1,b1 being Element of P1 for a2,b2 being Element of P2 st a1 = a2 & b1 = b2
holds (a1 <= b1 implies a2 <= b2) & (a1 < b1 implies a2 < b2);
theorem :: YELLOW_0:2
for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 for
X being set for a1 being Element of P1 for a2 being Element of P2 st a1 = a2
holds (X is_<=_than a1 implies X is_<=_than a2) & (X is_>=_than a1 implies X
is_>=_than a2);
theorem :: YELLOW_0:3
for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 & P1 is
complete holds P2 is complete;
theorem :: YELLOW_0:4
for L being transitive RelStr, x,y being Element of L st x <= y
for X being set holds (y is_<=_than X implies x is_<=_than X) & (x is_>=_than X
implies y is_>=_than X);
theorem :: YELLOW_0:5
for L being non empty RelStr, X being set, x being Element of L
holds (x is_>=_than X iff x is_>=_than X /\ the carrier of L) & (x is_<=_than X
iff x is_<=_than X /\ the carrier of L);
theorem :: YELLOW_0:6
for L being RelStr, a being Element of L holds {} is_<=_than a &
{} is_>=_than a;
theorem :: YELLOW_0:7
for L being RelStr, a,b being Element of L holds (a is_<=_than {b
} iff a <= b) & (a is_>=_than {b} iff b <= a);
theorem :: YELLOW_0:8
for L being RelStr, a,b,c being Element of L holds (a is_<=_than
{b,c} iff a <= b & a <= c) & (a is_>=_than {b,c} iff b <= a & c <= a);
theorem :: YELLOW_0:9
for L being RelStr, X,Y being set st X c= Y for x being Element
of L holds (x is_<=_than Y implies x is_<=_than X) & (x is_>=_than Y implies x
is_>=_than X);
theorem :: YELLOW_0:10
for L being RelStr, X,Y being set, x being Element of L holds (x
is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y) & (x is_>=_than X &
x is_>=_than Y implies x is_>=_than X \/ Y);
theorem :: YELLOW_0:11
for L being transitive RelStr for X being set, x,y being Element
of L st X is_<=_than x & x <= y holds X is_<=_than y;
theorem :: YELLOW_0:12
for L being transitive RelStr for X being set, x,y being Element
of L st X is_>=_than x & x >= y holds X is_>=_than y;
registration
let L be non empty RelStr;
cluster [#]L -> non empty;
end;
begin :: Least upper and greatest lower bounds
definition
let L be RelStr;
attr L is lower-bounded means
:: YELLOW_0:def 4
ex x being Element of L st x is_<=_than the carrier of L;
attr L is upper-bounded means
:: YELLOW_0:def 5
ex x being Element of L st x is_>=_than the carrier of L;
end;
definition
let L be RelStr;
attr L is bounded means
:: YELLOW_0:def 6
L is lower-bounded upper-bounded;
end;
theorem :: YELLOW_0:13
for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 holds (
P1 is lower-bounded implies P2 is lower-bounded) & (P1 is upper-bounded implies
P2 is upper-bounded);
registration
cluster complete -> bounded for non empty RelStr;
cluster bounded -> lower-bounded upper-bounded for RelStr;
cluster lower-bounded upper-bounded -> bounded for RelStr;
end;
registration
cluster complete for non empty Poset;
end;
definition
let L be RelStr;
let X be set;
pred ex_sup_of X,L means
:: YELLOW_0:def 7
ex a being Element of L st X is_<=_than a &
(for b being Element of L st X is_<=_than b holds b >= a) & for c being Element
of L st X is_<=_than c & for b being Element of L st X is_<=_than b holds b >=
c holds c = a;
pred ex_inf_of X,L means
:: YELLOW_0:def 8
ex a being Element of L st X is_>=_than a &
(for b being Element of L st X is_>=_than b holds b <= a) & for c being Element
of L st X is_>=_than c & for b being Element of L st X is_>=_than b holds b <=
c holds c = a;
end;
theorem :: YELLOW_0:14
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
for X being set holds (ex_sup_of X,L1 implies ex_sup_of X,L2) & (ex_inf_of X,L1
implies ex_inf_of X,L2);
theorem :: YELLOW_0:15
for L being antisymmetric RelStr, X being set holds ex_sup_of X,
L iff ex a being Element of L st X is_<=_than a & for b being Element of L st X
is_<=_than b holds a <= b;
theorem :: YELLOW_0:16
for L being antisymmetric RelStr, X being set holds ex_inf_of X,
L iff ex a being Element of L st X is_>=_than a & for b being Element of L st X
is_>=_than b holds a >= b;
theorem :: YELLOW_0:17
for L being complete non empty antisymmetric RelStr, X being set
holds ex_sup_of X,L & ex_inf_of X,L;
theorem :: YELLOW_0:18
for L being antisymmetric RelStr for a,b,c being Element of L
holds c = a"\/"b & ex_sup_of {a,b},L iff c >= a & c >= b & for d being Element
of L st d >= a & d >= b holds c <= d;
theorem :: YELLOW_0:19
for L being antisymmetric RelStr for a,b,c being Element of L
holds c = a"/\"b & ex_inf_of {a,b},L iff c <= a & c <= b & for d being Element
of L st d <= a & d <= b holds c >= d;
theorem :: YELLOW_0:20
for L being antisymmetric RelStr holds L is with_suprema iff for
a,b being Element of L holds ex_sup_of {a,b},L;
theorem :: YELLOW_0:21
for L being antisymmetric RelStr holds L is with_infima iff for
a,b being Element of L holds ex_inf_of {a,b},L;
theorem :: YELLOW_0:22
for L being antisymmetric with_suprema RelStr for a,b,c being
Element of L holds c = a"\/"b iff c >= a & c >= b & for d being Element of L st
d >= a & d >= b holds c <= d;
theorem :: YELLOW_0:23
for L being antisymmetric with_infima RelStr for a,b,c being
Element of L holds c = a"/\"b iff c <= a & c <= b & for d being Element of L st
d <= a & d <= b holds c >= d;
theorem :: YELLOW_0:24
for L being antisymmetric reflexive with_suprema RelStr for a,b being
Element of L holds a = a"\/"b iff a >= b;
theorem :: YELLOW_0:25
for L being antisymmetric reflexive with_infima RelStr for a,b being
Element of L holds a = a"/\"b iff a <= b;
definition
let L be RelStr;
let X be set;
func "\/"(X,L) -> Element of L means
:: YELLOW_0:def 9 :: Definition 1.1
X is_<=_than it & for a being
Element of L st X is_<=_than a holds it <= a if ex_sup_of X,L;
func "/\"(X,L) -> Element of L means
:: YELLOW_0:def 10
X is_>=_than it & for a being
Element of L st X is_>=_than a holds a <= it if ex_inf_of X,L;
end;
theorem :: YELLOW_0:26
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X
being set st ex_sup_of X,L1 holds "\/"(X,L1) = "\/"(X,L2);
theorem :: YELLOW_0:27
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X
being set st ex_inf_of X,L1 holds "/\"(X,L1) = "/\"(X,L2);
theorem :: YELLOW_0:28
for L being complete non empty Poset, X being set holds "\/"(X,L) =
"\/"(X, latt L) & "/\"(X,L) = "/\"(X, latt L);
theorem :: YELLOW_0:29
for L being complete Lattice, X being set holds "\/"(X,L) = "\/"(X,
LattPOSet L) & "/\"(X,L) = "/\"(X, LattPOSet L);
theorem :: YELLOW_0:30
for L being antisymmetric RelStr for a being Element of L, X
being set holds a = "\/"(X,L) & ex_sup_of X,L iff a is_>=_than X & for b being
Element of L st b is_>=_than X holds a <= b;
theorem :: YELLOW_0:31
for L being antisymmetric RelStr for a being Element of L, X
being set holds a = "/\"(X,L) & ex_inf_of X,L iff a is_<=_than X & for b being
Element of L st b is_<=_than X holds a >= b;
theorem :: YELLOW_0:32
for L being complete antisymmetric non empty RelStr for a being
Element of L, X being set holds a = "\/"(X,L) iff a is_>=_than X & for b being
Element of L st b is_>=_than X holds a <= b;
theorem :: YELLOW_0:33
for L being complete antisymmetric non empty RelStr for a being
Element of L, X being set holds a = "/\"(X,L) iff a is_<=_than X & for b being
Element of L st b is_<=_than X holds a >= b;
theorem :: YELLOW_0:34
for L being RelStr, X,Y being set st X c= Y & ex_sup_of X,L &
ex_sup_of Y,L holds "\/"(X,L) <= "\/"(Y,L);
theorem :: YELLOW_0:35
for L being RelStr, X,Y being set st X c= Y & ex_inf_of X,L &
ex_inf_of Y,L holds "/\"(X,L) >= "/\"(Y,L);
theorem :: YELLOW_0:36
for L being antisymmetric transitive RelStr, X,Y being set st
ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y, L holds "\/"(X \/ Y, L) =
"\/"(X,L)"\/""\/"(Y,L);
theorem :: YELLOW_0:37
for L being antisymmetric transitive RelStr, X,Y being set st
ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y, L holds "/\"(X \/ Y, L) =
"/\"(X,L) "/\" "/\"(Y,L);
notation
let L be RelStr;
let X be Subset of L;
synonym sup X for "\/"(X,L);
synonym inf X for "/\"(X,L);
end;
theorem :: YELLOW_0:38
for L being non empty reflexive antisymmetric RelStr for a being
Element of L holds ex_sup_of {a},L & ex_inf_of {a},L;
theorem :: YELLOW_0:39
for L being non empty reflexive antisymmetric RelStr for a being
Element of L holds sup {a} = a & inf {a} = a;
theorem :: YELLOW_0:40
for L being with_infima Poset, a,b being Element of L holds inf
{a,b} = a"/\"b;
theorem :: YELLOW_0:41
for L being with_suprema Poset, a,b being Element of L holds sup
{a,b} = a"\/" b;
theorem :: YELLOW_0:42
for L being lower-bounded antisymmetric non empty RelStr holds
ex_sup_of {},L & ex_inf_of the carrier of L, L;
theorem :: YELLOW_0:43
for L being upper-bounded antisymmetric non empty RelStr holds
ex_inf_of {},L & ex_sup_of the carrier of L, L;
definition
let L be RelStr;
func Bottom L -> Element of L equals
:: YELLOW_0:def 11
"\/"({},L);
func Top L -> Element of L equals
:: YELLOW_0:def 12
"/\"({},L);
end;
theorem :: YELLOW_0:44
for L being lower-bounded antisymmetric non empty RelStr for x being
Element of L holds Bottom L <= x;
theorem :: YELLOW_0:45
for L being upper-bounded antisymmetric non empty RelStr for x being
Element of L holds x <= Top L;
theorem :: YELLOW_0:46
for L being non empty RelStr, X,Y being set st for x being
Element of L holds x is_>=_than X iff x is_>=_than Y holds ex_sup_of X,L
implies ex_sup_of Y,L;
theorem :: YELLOW_0:47
for L being non empty RelStr, X,Y being set st ex_sup_of X,L &
for x being Element of L holds x is_>=_than X iff x is_>=_than Y holds "\/"(X,L
) = "\/"(Y,L);
theorem :: YELLOW_0:48
for L being non empty RelStr, X,Y being set st for x being
Element of L holds x is_<=_than X iff x is_<=_than Y holds ex_inf_of X,L
implies ex_inf_of Y,L;
theorem :: YELLOW_0:49
for L being non empty RelStr, X,Y being set st ex_inf_of X,L &
for x being Element of L holds x is_<=_than X iff x is_<=_than Y holds "/\"(X,L
) = "/\"(Y,L);
theorem :: YELLOW_0:50
for L being non empty RelStr, X being set holds (ex_sup_of X,L
iff ex_sup_of X /\ the carrier of L, L) & (ex_inf_of X,L iff ex_inf_of X /\ the
carrier of L, L);
theorem :: YELLOW_0:51
for L being non empty RelStr, X being set st ex_sup_of X,L or
ex_sup_of X /\ the carrier of L, L holds "\/"(X,L) = "\/"(X /\ the carrier of L
, L);
theorem :: YELLOW_0:52
for L being non empty RelStr, X being set st ex_inf_of X,L or
ex_inf_of X /\ the carrier of L, L holds "/\"(X,L) = "/\"(X /\ the carrier of L
, L);
theorem :: YELLOW_0:53
for L being non empty RelStr st for X being Subset of L holds
ex_sup_of X,L holds L is complete;
theorem :: YELLOW_0:54
for L being non empty Poset holds L is with_suprema iff for X being
finite non empty Subset of L holds ex_sup_of X,L;
theorem :: YELLOW_0:55
for L being non empty Poset holds L is with_infima iff for X being
finite non empty Subset of L holds ex_inf_of X,L;
begin
definition
let L be RelStr;
mode SubRelStr of L -> RelStr means
:: YELLOW_0:def 13
the carrier of it c= the carrier
of L & the InternalRel of it c= the InternalRel of L;
end;
definition
let L be RelStr;
let S be SubRelStr of L;
attr S is full means
:: YELLOW_0:def 14
the InternalRel of S = (the InternalRel of L) |_2 the carrier of S;
end;
registration
let L be RelStr;
cluster strict full for SubRelStr of L;
end;
registration
let L be non empty RelStr;
cluster non empty full strict for SubRelStr of L;
end;
theorem :: YELLOW_0:56
for L being RelStr, X being Subset of L holds RelStr(#X, (the
InternalRel of L)|_2 X#) is full SubRelStr of L;
theorem :: YELLOW_0:57
for L being RelStr, S1,S2 being full SubRelStr of L st the
carrier of S1 = the carrier of S2 holds the RelStr of S1 = the RelStr of S2;
definition
let L be RelStr;
let X be Subset of L;
func subrelstr X -> full strict SubRelStr of L means
:: YELLOW_0:def 15
the carrier of it = X;
end;
theorem :: YELLOW_0:58
for L being non empty RelStr, S being non empty SubRelStr of L
for x being Element of S holds x is Element of L;
theorem :: YELLOW_0:59
for L being RelStr, S being SubRelStr of L for a,b being Element
of L for x,y being Element of S st x = a & y = b & x <= y holds a <= b;
theorem :: YELLOW_0:60
for L being RelStr, S being full SubRelStr of L for a,b being
Element of L for x,y being Element of S st x = a & y = b & a <= b & x in the
carrier of S holds x <= y;
theorem :: YELLOW_0:61
for L being non empty RelStr, S being non empty full SubRelStr
of L for X being set, a being Element of L for x being Element of S st x = a
holds (a is_<=_than X implies x is_<=_than X) & (a is_>=_than X implies x
is_>=_than X);
theorem :: YELLOW_0:62
for L being non empty RelStr, S being non empty SubRelStr of L
for X being Subset of S for a being Element of L for x being Element of S st x
= a holds (x is_<=_than X implies a is_<=_than X) & (x is_>=_than X implies a
is_>=_than X);
registration
let L be reflexive RelStr;
cluster -> reflexive for full SubRelStr of L;
end;
registration
let L be transitive RelStr;
cluster -> transitive for full SubRelStr of L;
end;
registration
let L be antisymmetric RelStr;
cluster -> antisymmetric for full SubRelStr of L;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is meet-inheriting means
:: YELLOW_0:def 16
for x,y being Element of L st x in
the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds inf {x,y} in
the carrier of S;
attr S is join-inheriting means
:: YELLOW_0:def 17
for x,y being Element of L st x in
the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds sup {x,y} in
the carrier of S;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is infs-inheriting means
:: YELLOW_0:def 18
for X being Subset of S st ex_inf_of X,L holds "/\"(X,L) in the carrier of S;
attr S is sups-inheriting means
:: YELLOW_0:def 19
for X being Subset of S st ex_sup_of X,L holds "\/"(X,L) in the carrier of S;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting -> meet-inheriting for SubRelStr of L;
cluster sups-inheriting -> join-inheriting for SubRelStr of L;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting sups-inheriting non empty full strict for
SubRelStr of L;
end;
theorem :: YELLOW_0:63
for L being non empty transitive RelStr for S being non empty
full SubRelStr of L for X being Subset of S st ex_inf_of X,L & "/\"(X,L) in the
carrier of S holds ex_inf_of X,S & "/\"(X,S) = "/\"(X,L);
theorem :: YELLOW_0:64
for L being non empty transitive RelStr for S being non empty
full SubRelStr of L for X being Subset of S st ex_sup_of X,L & "\/"(X,L) in the
carrier of S holds ex_sup_of X,S & "\/"(X,S) = "\/"(X,L);
theorem :: YELLOW_0:65
for L being non empty transitive RelStr for S being non empty full
SubRelStr of L for x,y being Element of S st ex_inf_of {x,y},L & "/\"({x,y},L)
in the carrier of S holds ex_inf_of {x,y},S & "/\"({x,y},S) = "/\"({x,y},L);
theorem :: YELLOW_0:66
for L being non empty transitive RelStr for S being non empty full
SubRelStr of L for x,y being Element of S st ex_sup_of {x,y},L & "\/"({x,y},L)
in the carrier of S holds ex_sup_of {x,y},S & "\/"({x,y},S) = "\/"({x,y},L);
registration
let L be with_infima antisymmetric transitive RelStr;
cluster -> with_infima for non empty meet-inheriting full SubRelStr of L;
end;
registration
let L be with_suprema antisymmetric transitive RelStr;
cluster -> with_suprema for non empty join-inheriting full SubRelStr of L;
end;
theorem :: YELLOW_0:67
for L being complete non empty Poset for S being non empty full
SubRelStr of L for X being Subset of S st "/\"(X,L) in the carrier of S holds
"/\"(X,S) = "/\"(X,L);
theorem :: YELLOW_0:68
for L being complete non empty Poset for S being non empty full
SubRelStr of L for X being Subset of S st "\/"(X,L) in the carrier of S holds
"\/"(X,S) = "\/"(X,L);
theorem :: YELLOW_0:69
for L being with_infima Poset for S being meet-inheriting non empty
full SubRelStr of L for x,y being Element of S, a,b be Element of L st a = x &
b = y holds x"/\"y = a"/\"b;
theorem :: YELLOW_0:70
for L being with_suprema Poset for S being join-inheriting non empty
full SubRelStr of L for x,y being Element of S, a,b be Element of L st a = x &
b = y holds x"\/"y = a"\/"b;