:: Bounds in Posets and Relational Substructures
:: by Grzegorz Bancerek
::
:: Received September 10, 1996
:: Copyright (c) 1996-2026 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;
definitions STRUCT_0, RELAT_2, ORDERS_2, LATTICE3;
equalities LATTICE3, WELLORD1;
expansions STRUCT_0, RELAT_2, ORDERS_2, LATTICE3;
theorems TARSKI, ZFMISC_1, ORDERS_2, LATTICE3, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FINSET_1, RELSET_1;
begin :: Reexamination of poset concepts
scheme
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] proof
consider R being Relation of X() such that
A1: for a,b being Element of X() holds [a,b] in R iff P[a,b] from
RELSET_1:sch 2;
take L = RelStr(#X(),R#);
thus the carrier of L = X();
let a,b be Element of L;
thus thesis by A1;
end;
definition
let A be non empty RelStr;
redefine attr A is reflexive means :: redefines reflexive (ORDERS_2, definition)
for x being Element of A holds x <= x;
compatibility
proof
thus A is reflexive implies for x being Element of A holds x <= x by
ORDERS_2:1;
assume
A1: for x being Element of A holds x <= x;
let x be object;
assume x in the carrier of A;
then reconsider x as Element of A;
x <= x by A1;
hence thesis;
end;
end;
definition
let A be RelStr;
redefine attr A is transitive means :: redefines transitive (ORDERS_2, definition)
for x,y,z being Element of A st x <= y & y <= z holds x <= z;
compatibility
proof
thus A is transitive implies for x,y,z being Element of A st x <= y & y <=
z holds x <= z by ORDERS_2:3;
assume
A1: for x,y,z being Element of A st x <= y & y <= z holds x <= z;
let x,y,z be object;
assume
A2: x in the carrier of A & y in the carrier of A & z in the carrier of A;
assume
A3: [x,y] in the InternalRel of A & [y,z] in the InternalRel of A;
reconsider x,y,z as Element of A by A2;
x <= y & y <= z by A3;
then x <= z by A1;
hence thesis;
end;
redefine attr A is antisymmetric means :: redefines antisymmetric (ORDERS_2, definition)
for x,y being Element of A st x <= y & y <= x holds x = y;
compatibility
proof
thus A is antisymmetric implies for x,y being Element of A st x <= y & y
<= x holds x = y by ORDERS_2:2;
assume
A4: for x,y being Element of A st x <= y & y <= x holds x = y;
let x,y be object;
assume
A5: x in the carrier of A & y in the carrier of A;
assume
A6: [x,y] in the InternalRel of A & [y,x] in the InternalRel of A;
reconsider x,y as Element of A by A5;
x <= y & y <= x by A6;
hence thesis by A4;
end;
end;
registration
cluster complete -> with_suprema with_infima for non empty RelStr;
coherence by LATTICE3:12;
cluster -> complete transitive antisymmetric
for 1-element reflexive RelStr;
coherence
proof
let L be 1-element reflexive RelStr;
set x = the Element of L;
A1: for x,y being Element of L holds x = y by STRUCT_0:def 10;
thus L is complete
proof
let X be set;
take x;
thus for y be Element of L st y in X holds y <= x by A1;
let y be Element of L;
y = x by A1;
hence thesis by ORDERS_2:1;
end;
thus L is transitive
by A1;
let x be Element of L;
thus thesis by A1;
end;
end;
registration
let x be set;
let R be Relation of {x};
cluster RelStr(#{x},R#) -> 1-element;
coherence;
end;
registration
cluster strict 1-element reflexive for RelStr;
existence
proof
set O = the Order of {{}};
take RelStr(#{{}}, O#);
thus thesis;
end;
end;
theorem Th1:
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)
proof
let P1,P2 be RelStr such that
A1: the RelStr of P1 = the RelStr of P2;
let a1,b1 be Element of P1;
let a2,b2 be Element of P2;
A2: a2 <= b2 iff [a2,b2] in the InternalRel of P2;
a1 <= b1 iff [a1,b1] in the InternalRel of P1;
hence thesis by A1,A2;
end;
theorem Th2:
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)
by Th1;
theorem
for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 & P1 is
complete holds P2 is complete
proof
let P1,P2 be RelStr such that
A1: the RelStr of P1 = the RelStr of P2 and
A2: for X being set ex a being Element of P1 st X is_<=_than a & for b
being Element of P1 st X is_<=_than b holds a <= b;
let X be set;
consider a being Element of P1 such that
A3: X is_<=_than a and
A4: for b being Element of P1 st X is_<=_than b holds a <= b by A2;
reconsider a9 = a as Element of P2 by A1;
take a9;
thus X is_<=_than a9 by A1,A3,Th2;
let b9 be Element of P2;
reconsider b = b9 as Element of P1 by A1;
assume X is_<=_than b9;
then a <= b by A1,A4,Th2;
hence thesis by A1;
end;
theorem Th4:
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)
proof
let L be transitive RelStr, x,y be Element of L;
assume
A1: x <= y;
let X be set;
hereby
assume
A2: y is_<=_than X;
thus x is_<=_than X
proof
let z be Element of L;
assume z in X;
then z >= y by A2;
hence thesis by A1,ORDERS_2:3;
end;
end;
assume
A3: x is_>=_than X;
let z be Element of L;
assume z in X;
then x >= z by A3;
hence thesis by A1,ORDERS_2:3;
end;
theorem Th5:
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)
proof
let L be non empty RelStr, X be set, x be Element of L;
set Y = X /\ the carrier of L;
thus X is_<=_than x implies Y is_<=_than x
proof
assume
A1: for b being Element of L st b in X holds b <= x;
let b be Element of L;
assume b in Y;
then b in X by XBOOLE_0:def 4;
hence thesis by A1;
end;
thus Y is_<=_than x implies X is_<=_than x
proof
assume
A2: for b being Element of L st b in Y holds b <= x;
let b be Element of L;
assume b in X;
then b in Y by XBOOLE_0:def 4;
hence thesis by A2;
end;
thus X is_>=_than x implies Y is_>=_than x
proof
assume
A3: for b being Element of L st b in X holds b >= x;
let b be Element of L;
assume b in Y;
then b in X by XBOOLE_0:def 4;
hence thesis by A3;
end;
thus Y is_>=_than x implies X is_>=_than x
proof
assume
A4: for b being Element of L st b in Y holds b >= x;
let b be Element of L;
assume b in X;
then b in Y by XBOOLE_0:def 4;
hence thesis by A4;
end;
end;
theorem Th6:
for L being RelStr, a being Element of L holds {} is_<=_than a &
{} is_>=_than a;
theorem Th7:
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)
proof
let L be RelStr, a,b be Element of L;
A1: b in {b} by TARSKI:def 1;
hence a is_<=_than {b} implies a <= b;
thus a <= b implies a is_<=_than {b} by TARSKI:def 1;
thus a is_>=_than {b} implies a >= b by A1;
assume
A2: a >= b;
let c be Element of L;
thus thesis by A2,TARSKI:def 1;
end;
theorem Th8:
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)
proof
let L be RelStr, a,b,c be Element of L;
A1: b in {b,c} & c in {b,c} by TARSKI:def 2;
hence a is_<=_than {b,c} implies a <= b & a <= c;
thus a <= b & a <= c implies a is_<=_than {b,c} by TARSKI:def 2;
thus a is_>=_than {b,c} implies a >= b & a >= c by A1;
assume
A2: a >= b & a >= c;
let c be Element of L;
thus thesis by A2,TARSKI:def 2;
end;
theorem
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 Th10:
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)
proof
let L be RelStr, X,Y be set, x be Element of L;
thus x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y
proof
assume
A1: ( for y being Element of L st y in X holds y >= x)& for y being
Element of L st y in Y holds y >= x;
let y be Element of L;
y in X \/ Y implies y in X or y in Y by XBOOLE_0:def 3;
hence thesis by A1;
end;
assume
A2: ( for y being Element of L st y in X holds y <= x)& for y being
Element of L st y in Y holds y <= x;
let y be Element of L;
y in X \/ Y implies y in X or y in Y by XBOOLE_0:def 3;
hence thesis by A2;
end;
theorem Th11:
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
proof
let L be transitive RelStr;
let X be set, x,y be Element of L such that
A1: for y being Element of L st y in X holds y <= x and
A2: x <= y;
let z be Element of L;
assume z in X;
then z <= x by A1;
hence thesis by A2,ORDERS_2:3;
end;
theorem Th12:
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
proof
let L be transitive RelStr;
let X be set, x,y be Element of L such that
A1: for y being Element of L st y in X holds y >= x and
A2: x >= y;
let z be Element of L;
assume z in X;
then z >= x by A1;
hence thesis by A2,ORDERS_2:3;
end;
registration
let L be non empty RelStr;
cluster [#]L -> non empty;
coherence;
end;
begin :: Least upper and greatest lower bounds
definition
let L be RelStr;
attr L is lower-bounded means
:Def4:
ex x being Element of L st x is_<=_than the carrier of L;
attr L is upper-bounded means
:Def5:
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
L is lower-bounded upper-bounded;
end;
theorem
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)
by Th2;
registration
cluster complete -> bounded for non empty RelStr;
coherence
proof
let L be non empty RelStr;
assume
A1: for X being set 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;
then consider a0 being Element of L such that
{} is_<=_than a0 and
A2: for b being Element of L st {} is_<=_than b holds a0 <= b;
consider a1 being Element of L such that
A3: the carrier of L is_<=_than a1 and
for b being Element of L st the carrier of L is_<=_than b holds a1 <=
b by A1;
reconsider a0, a1 as Element of L;
hereby
take a0;
thus a0 is_<=_than the carrier of L
by A2,Th6;
end;
take a1;
thus thesis by A3;
end;
cluster bounded -> lower-bounded upper-bounded for RelStr;
coherence;
cluster lower-bounded upper-bounded -> bounded for RelStr;
coherence;
end;
registration
cluster complete for non empty Poset;
existence
proof
set L = the complete non empty Poset;
take L;
thus thesis;
end;
end;
definition
let L be RelStr;
let X be set;
pred ex_sup_of X,L means
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
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 Th14:
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)
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X be set;
thus ex_sup_of X,L1 implies ex_sup_of X,L2
proof
given a being Element of L1 such that
A2: X is_<=_than a and
A3: for b being Element of L1 st X is_<=_than b holds b >= a and
A4: for c being Element of L1 st X is_<=_than c & for b being Element
of L1 st X is_<=_than b holds b >= c holds c = a;
reconsider a9 = a as Element of L2 by A1;
take a9;
thus X is_<=_than a9 by A1,A2,Th2;
hereby
let b9 be Element of L2;
reconsider b = b9 as Element of L1 by A1;
assume X is_<=_than b9;
then b >= a by A1,A3,Th2;
hence b9 >= a9 by A1;
end;
let c9 be Element of L2;
reconsider c = c9 as Element of L1 by A1;
assume X is_<=_than c9;
then
A5: X is_<=_than c by A1,Th2;
assume
A6: for b9 being Element of L2 st X is_<=_than b9 holds b9 >= c9;
now
let b be Element of L1;
reconsider b9 = b as Element of L2 by A1;
assume X is_<=_than b;
then b9 >= c9 by A1,A6,Th2;
hence b >= c by A1;
end;
hence thesis by A4,A5;
end;
given a being Element of L1 such that
A7: X is_>=_than a and
A8: for b being Element of L1 st X is_>=_than b holds b <= a and
A9: for c being Element of L1 st X is_>=_than c & for b being Element
of L1 st X is_>=_than b holds b <= c holds c = a;
reconsider a9 = a as Element of L2 by A1;
take a9;
thus X is_>=_than a9 by A1,A7,Th2;
hereby
let b9 be Element of L2;
reconsider b = b9 as Element of L1 by A1;
assume X is_>=_than b9;
then b <= a by A1,A8,Th2;
hence b9 <= a9 by A1;
end;
let c9 be Element of L2;
reconsider c = c9 as Element of L1 by A1;
assume
A10: X is_>=_than c9;
assume
A11: for b9 being Element of L2 st X is_>=_than b9 holds b9 <= c9;
A12: now
let b be Element of L1;
reconsider b9 = b as Element of L2 by A1;
assume X is_>=_than b;
then b9 <= c9 by A1,A11,Th2;
hence b <= c by A1;
end;
X is_>=_than c by A1,A10,Th2;
hence thesis by A9,A12;
end;
theorem Th15:
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
proof
let L be antisymmetric RelStr, X be set;
thus ex_sup_of X,L implies
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;
given a being Element of L such that
A1: X is_<=_than a & for b being Element of L st X is_<=_than b holds a <= b;
take a;
thus X is_<=_than a & for b being Element of L st X is_<=_than b holds b >=
a by A1;
let c be Element of L;
assume
X is_<=_than c & for b being Element of L st X is_<=_than b holds b >= c;
then a <= c & c <= a by A1;
hence thesis by ORDERS_2:2;
end;
theorem Th16:
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
proof
let L be antisymmetric RelStr, X be set;
thus ex_inf_of X,L implies
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;
given a being Element of L such that
A1: X is_>=_than a & for b being Element of L st X is_>=_than b holds a >= b;
take a;
thus X is_>=_than a & for b being Element of L st X is_>=_than b holds a >=
b by A1;
let c be Element of L;
assume
X is_>=_than c & for b being Element of L st X is_>=_than b holds c >= b;
then a <= c & c <= a by A1;
hence thesis by ORDERS_2:2;
end;
theorem Th17:
for L being complete non empty antisymmetric RelStr, X being set
holds ex_sup_of X,L & ex_inf_of X,L
proof
let L be complete non empty antisymmetric RelStr, X be set;
set Y = {c where c is Element of L: c is_<=_than X};
consider a being Element of L such that
A1: Y is_<=_than a and
A2: for b being Element of L st Y is_<=_than b holds a <= b by LATTICE3:def 12;
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 by LATTICE3:def 12;
hence ex_sup_of X,L by Th15;
now
take a;
thus a is_<=_than X
proof
let b be Element of L;
assume
A3: b in X;
Y is_<=_than b
proof
let c be Element of L;
assume c in Y;
then ex d being Element of L st c = d & d is_<=_than X;
hence thesis by A3;
end;
hence thesis by A2;
end;
let b be Element of L;
assume b is_<=_than X;
then b in Y;
hence b <= a by A1;
end;
hence thesis by Th16;
end;
theorem Th18:
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
proof
let L be antisymmetric RelStr;
let a,b,c be Element of L;
hereby
assume that
A1: c = a"\/"b and
A2: ex_sup_of {a,b},L;
consider c1 being Element of L such that
A3: {a,b} is_<=_than c1 and
A4: for d being Element of L st {a,b} is_<=_than d holds c1 <= d by A2;
A5: now
let d be Element of L;
assume a <= d & b <= d;
then {a,b} is_<=_than d by Th8;
hence c1 <= d by A4;
end;
a <= c1 & b <= c1 by A3,Th8;
hence
c >= a & c >= b & for d being Element of L st d >= a & d >= b holds c
<= d by A1,A5,LATTICE3:def 13;
end;
assume that
A6: c >= a & c >= b and
A7: for d being Element of L st d >= a & d >= b holds c <= d;
thus c = a"\/"b by A6,A7,LATTICE3:def 13;
now
take c;
thus c is_>=_than {a,b} by A6,Th8;
let d be Element of L;
assume d is_>=_than {a,b};
then d >= a & d >= b by Th8;
hence c <= d by A7;
end;
hence thesis by Th15;
end;
theorem Th19:
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
proof
let L be antisymmetric RelStr;
let a,b,c be Element of L;
hereby
assume that
A1: c = a"/\"b and
A2: ex_inf_of {a,b},L;
consider c1 being Element of L such that
A3: {a,b} is_>=_than c1 and
A4: for d being Element of L st {a,b} is_>=_than d holds c1 >= d by A2;
A5: now
let d be Element of L;
assume a >= d & b >= d;
then {a,b} is_>=_than d by Th8;
hence c1 >= d by A4;
end;
a >= c1 & b >= c1 by A3,Th8;
hence
c <= a & c <= b & for d being Element of L st d <= a & d <= b holds c
>= d by A1,A5,LATTICE3:def 14;
end;
assume that
A6: c <= a & c <= b and
A7: for d being Element of L st d <= a & d <= b holds c >= d;
thus c = a"/\"b by A6,A7,LATTICE3:def 14;
now
take c;
thus c is_<=_than {a,b} by A6,Th8;
let d be Element of L;
assume d is_<=_than {a,b};
then d <= a & d <= b by Th8;
hence c >= d by A7;
end;
hence thesis by Th16;
end;
theorem Th20:
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
proof
let L be antisymmetric RelStr;
hereby
assume
A1: L is with_suprema;
let a,b be Element of L;
ex z being Element of L st a <= z & b <= z & for z9 being Element of L
st a <= z9 & b <= z9 holds z <= z9 by A1;
hence ex_sup_of {a,b},L by Th18;
end;
assume
A2: for a,b being Element of L holds ex_sup_of {a,b},L;
let x,y be Element of L;
take x"\/"y;
ex_sup_of {x,y},L by A2;
hence thesis by Th18;
end;
theorem Th21:
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
proof
let L be antisymmetric RelStr;
hereby
assume
A1: L is with_infima;
let a,b be Element of L;
ex z being Element of L st a >= z & b >= z & for z9 being Element of L
st a >= z9 & b >= z9 holds z >= z9 by A1;
hence ex_inf_of {a,b},L by Th19;
end;
assume
A2: for a,b being Element of L holds ex_inf_of {a,b},L;
let x,y be Element of L;
take x"/\"y;
ex_inf_of {x,y},L by A2;
hence thesis by Th19;
end;
theorem Th22:
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
proof
let A be antisymmetric with_suprema RelStr;
let a,b be Element of A;
ex x being Element of A st a <= x & b <= x & for c being Element of A st
a <= c & b <= c holds x <= c by LATTICE3:def 10;
hence thesis by LATTICE3:def 13;
end;
theorem Th23:
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
proof
let A be antisymmetric with_infima RelStr;
let a,b be Element of A;
ex x being Element of A st a >= x & b >= x & for c being Element of A st
a >= c & b >= c holds x >= c by LATTICE3:def 11;
hence thesis by LATTICE3:def 14;
end;
theorem
for L being antisymmetric reflexive with_suprema RelStr for a,b being
Element of L holds a = a"\/"b iff a >= b
proof
let L be antisymmetric reflexive with_suprema RelStr;
let a,b be Element of L;
a <= a & for d being Element of L st d >= a & d >= b holds a <= d;
hence thesis by Th22;
end;
theorem
for L being antisymmetric reflexive with_infima RelStr for a,b being
Element of L holds a = a"/\"b iff a <= b
proof
let L be antisymmetric reflexive with_infima RelStr;
let a,b be Element of L;
a <= a & for d being Element of L st d <= a & d <= b holds a >= d;
hence thesis by Th23;
end;
definition
let L be RelStr;
let X be set;
func "\/"(X,L) -> Element of L means :: Definition 1.1
:Def9:
X is_<=_than it & for a being
Element of L st X is_<=_than a holds it <= a if ex_sup_of X,L;
uniqueness
proof
let a1,a2 be Element of L;
given a being Element of L such that
X is_<=_than a and
for b being Element of L st X is_<=_than b holds b >= a and
A1: 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;
assume
A2: not thesis;
then a1 = a by A1;
hence contradiction by A1,A2;
end;
existence;
correctness;
func "/\"(X,L) -> Element of L means
:Def10:
X is_>=_than it & for a being
Element of L st X is_>=_than a holds a <= it if ex_inf_of X,L;
uniqueness
proof
let a1,a2 be Element of L;
given a being Element of L such that
X is_>=_than a and
for b being Element of L st X is_>=_than b holds b <= a and
A3: 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;
assume
A4: not thesis;
then a1 = a by A3;
hence contradiction by A3,A4;
end;
existence;
correctness;
end;
theorem
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)
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X be set;
reconsider c = "\/"(X,L1) as Element of L2 by A1;
assume
A2: ex_sup_of X,L1;
then X is_<=_than "\/"(X,L1) by Def9;
then
A3: X is_<=_than c by A1,Th2;
A4: now
let a be Element of L2;
reconsider b = a as Element of L1 by A1;
assume X is_<=_than a;
then X is_<=_than b by A1,Th2;
then b >= "\/"(X,L1) by A2,Def9;
hence a >= c by A1;
end;
ex_sup_of X,L2 by A1,A2,Th14;
hence thesis by A3,A4,Def9;
end;
theorem
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)
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X be set;
reconsider c = "/\"(X,L1) as Element of L2 by A1;
assume
A2: ex_inf_of X,L1;
then X is_>=_than "/\"(X,L1) by Def10;
then
A3: X is_>=_than c by A1,Th2;
A4: now
let a be Element of L2;
reconsider b = a as Element of L1 by A1;
assume X is_>=_than a;
then X is_>=_than b by A1,Th2;
then b <= "/\"(X,L1) by A2,Def10;
hence a <= c by A1;
end;
ex_inf_of X,L2 by A1,A2,Th14;
hence thesis by A3,A4,Def10;
end;
theorem
for L being complete non empty Poset, X being set holds "\/"(X,L) =
"\/"(X, latt L) & "/\"(X,L) = "/\"(X, latt L)
proof
let L be complete non empty Poset, X be set;
A1: the RelStr of L = LattPOSet latt L by LATTICE3:def 15;
then reconsider x = "\/"(X,L) as Element of LattPOSet latt L;
reconsider y = "/\"(X,latt L) as Element of L by A1;
A2: now
let a be Element of L;
reconsider a9 = a as Element of LattPOSet latt L by A1;
assume a is_<=_than X;
then a9 is_<=_than X by A1,Th2;
then %a9 is_less_than X by LATTICE3:29;
then
A3: %a9 [= "/\"(X,latt L) by LATTICE3:34;
(%a9)% = %a9;
then a9 <= ("/\"(X,latt L))% by A3,LATTICE3:7;
hence a <= y by A1;
end;
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 by LATTICE3:def 12;
then
A4: ex_sup_of X,L by Th15;
A5: now
let a be Element of latt L;
reconsider a9 = a% as Element of L by A1;
assume X is_less_than a;
then X is_<=_than a% by LATTICE3:30;
then X is_<=_than a9 by A1,Th2;
then "\/"(X,L) <= a9 by A4,Def9;
then
A6: x <= a% by A1;
(%x)% = %x;
hence %x [= a by A6,LATTICE3:7;
end;
X is_<=_than "\/"(X,L) by A4,Def9;
then X is_<=_than x by A1,Th2;
then X is_less_than %x by LATTICE3:31;
hence "\/"(X,L) = "\/"(X, latt L) by A5,LATTICE3:def 21;
"/\"(X,latt L) is_less_than X by LATTICE3:34;
then ("/\"(X,latt L))% is_<=_than X by LATTICE3:28;
then
A7: y is_<=_than X by A1,Th2;
then ex_inf_of X,L by A2,Th16;
hence thesis by A7,A2,Def10;
end;
theorem
for L being complete Lattice, X being set holds "\/"(X,L) = "\/"(X,
LattPOSet L) & "/\"(X,L) = "/\"(X, LattPOSet L)
proof
let L be complete Lattice, X be set;
A1: now
let r be Element of LattPOSet L;
assume X is_<=_than r;
then X is_less_than %r by LATTICE3:31;
then
A2: "\/"(X,L) [= %r by LATTICE3:def 21;
(%r)% = %r;
hence ("\/"(X,L))% <= r by A2,LATTICE3:7;
end;
X is_less_than "\/"(X,L) by LATTICE3:def 21;
then
A3: X is_<=_than ("\/"(X,L))% by LATTICE3:30;
then ex_sup_of X, LattPOSet L by A1,Th15;
hence "\/"(X,L) = "\/"(X, LattPOSet L) by A3,A1,Def9;
A4: now
let r be Element of LattPOSet L;
assume X is_>=_than r;
then X is_greater_than %r by LATTICE3:29;
then
A5: %r [= "/\"(X,L) by LATTICE3:34;
(%r)% = %r;
hence ("/\"(X,L))% >= r by A5,LATTICE3:7;
end;
X is_greater_than "/\"(X,L) by LATTICE3:34;
then
A6: X is_>=_than ("/\"(X,L))% by LATTICE3:28;
then ex_inf_of X, LattPOSet L by A4,Th16;
hence thesis by A6,A4,Def10;
end;
theorem Th30:
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
proof
let L be antisymmetric RelStr;
let a be Element of L, X be set;
(a is_>=_than X & for b being Element of L st b is_>=_than X holds a <=
b ) implies ex_sup_of X,L by Th15;
hence thesis by Def9;
end;
theorem Th31:
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
proof
let L be antisymmetric RelStr;
let a be Element of L, X be set;
(a is_<=_than X & for b being Element of L st b is_<=_than X holds a >=
b ) implies ex_inf_of X,L by Th16;
hence thesis by Def10;
end;
theorem
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
proof
let L be complete antisymmetric non empty RelStr;
let a be Element of L, X be set;
ex_sup_of X,L by Th17;
hence thesis by Th30;
end;
theorem
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
proof
let L be complete non empty antisymmetric RelStr;
let a be Element of L, X be set;
ex_inf_of X,L by Th17;
hence thesis by Th31;
end;
theorem Th34:
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)
proof
let L be RelStr, X,Y be set;
assume that
A1: X c= Y and
A2: ex_sup_of X,L and
A3: ex_sup_of Y,L;
"\/"(Y,L) is_>=_than X
proof
let x be Element of L;
assume
A4: x in X;
"\/"(Y,L) is_>=_than Y by A3,Def9;
hence thesis by A1,A4;
end;
hence thesis by A2,Def9;
end;
theorem Th35:
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)
proof
let L be RelStr, X,Y be set;
assume that
A1: X c= Y and
A2: ex_inf_of X,L and
A3: ex_inf_of Y,L;
"/\"(Y,L) is_<=_than X
proof
let x be Element of L;
assume
A4: x in X;
"/\"(Y,L) is_<=_than Y by A3,Def10;
hence thesis by A1,A4;
end;
hence thesis by A2,Def10;
end;
theorem
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)
proof
let L be antisymmetric transitive RelStr;
let X,Y be set such that
A1: ex_sup_of X,L & ex_sup_of Y,L and
A2: ex_sup_of X \/ Y, L;
set a = "\/"(X,L), b = "\/"(Y,L), c = "\/"(X \/ Y, L);
A3: a is_>=_than X & b is_>=_than Y by A1,Th30;
A4: now
let d be Element of L;
assume d >= a & d >= b;
then d is_>=_than X & d is_>=_than Y by A3,Th4;
then d is_>=_than X \/ Y by Th10;
hence c <= d by A2,Th30;
end;
c >= a & c >= b by A1,A2,Th34,XBOOLE_1:7;
hence thesis by A4,Th18;
end;
theorem
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)
proof
let L be antisymmetric transitive RelStr;
let X,Y be set such that
A1: ex_inf_of X,L & ex_inf_of Y,L and
A2: ex_inf_of X \/ Y, L;
set a = "/\"(X,L), b = "/\"(Y,L), c = "/\"(X \/ Y, L);
A3: a is_<=_than X & b is_<=_than Y by A1,Th31;
A4: now
let d be Element of L;
assume d <= a & d <= b;
then d is_<=_than X & d is_<=_than Y by A3,Th4;
then d is_<=_than X \/ Y by Th10;
hence c >= d by A2,Th31;
end;
c <= a & c <= b by A1,A2,Th35,XBOOLE_1:7;
hence thesis by A4,Th19;
end;
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 Th38:
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
proof
let L be non empty reflexive antisymmetric RelStr, a be Element of L;
A1: for b being Element of L st b is_>=_than {a} holds b >= a by Th7;
A2: a <= a;
then a is_>=_than {a} by Th7;
hence ex_sup_of {a},L by A1,Th15;
A3: for b being Element of L st b is_<=_than {a} holds b <= a by Th7;
a is_<=_than {a} by A2,Th7;
hence thesis by A3,Th16;
end;
theorem
for L being non empty reflexive antisymmetric RelStr for a being
Element of L holds sup {a} = a & inf {a} = a
proof
let L be non empty reflexive antisymmetric RelStr;
let a be Element of L;
A1: for b being Element of L st b is_>=_than {a} holds b >= a by Th7;
A2: a <= a;
then a is_>=_than {a} by Th7;
hence sup {a} = a by A1,Th30;
A3: for b being Element of L st b is_<=_than {a} holds b <= a by Th7;
a is_<=_than {a} by A2,Th7;
hence thesis by A3,Th31;
end;
theorem Th40:
for L being with_infima Poset, a,b being Element of L holds inf
{a,b} = a"/\"b
proof
let L be with_infima Poset, a,b be Element of L;
A1: now
let c be Element of L;
assume c is_<=_than {a,b};
then c <= a & c <= b by Th8;
hence c <= a"/\"b by Th23;
end;
a"/\"b <= a & a"/\"b <= b by Th23;
then
A2: a"/\"b is_<=_than {a,b} by Th8;
then ex_inf_of {a,b}, L by A1,Th16;
hence thesis by A2,A1,Def10;
end;
theorem Th41:
for L being with_suprema Poset, a,b being Element of L holds sup
{a,b} = a"\/" b
proof
let L be with_suprema Poset, a,b be Element of L;
A1: now
let c be Element of L;
assume c is_>=_than {a,b};
then c >= a & c >= b by Th8;
hence c >= a"\/"b by Th22;
end;
a"\/"b >= a & a"\/"b >= b by Th22;
then
A2: a"\/"b is_>=_than {a,b} by Th8;
then ex_sup_of {a,b}, L by A1,Th15;
hence thesis by A2,A1,Def9;
end;
theorem Th42:
for L being lower-bounded antisymmetric non empty RelStr holds
ex_sup_of {},L & ex_inf_of the carrier of L, L
proof
let L be lower-bounded antisymmetric non empty RelStr;
consider a being Element of L such that
A1: a is_<=_than the carrier of L by Def4;
now
take a;
thus a is_>=_than {};
thus for b being Element of L st b is_>=_than {} holds a <= b by A1;
end;
hence ex_sup_of {},L by Th15;
for b being Element of L st the carrier of L is_>=_than b holds a >= b;
hence thesis by A1,Th16;
end;
theorem Th43:
for L being upper-bounded antisymmetric non empty RelStr holds
ex_inf_of {},L & ex_sup_of the carrier of L, L
proof
let L be upper-bounded antisymmetric non empty RelStr;
consider a being Element of L such that
A1: a is_>=_than the carrier of L by Def5;
now
take a;
thus a is_<=_than {};
thus for b being Element of L st b is_<=_than {} holds a >= b by A1;
end;
hence ex_inf_of {},L by Th16;
for b being Element of L st the carrier of L is_<=_than b holds a <= b;
hence thesis by A1,Th15;
end;
definition
let L be RelStr;
func Bottom L -> Element of L equals
"\/"({},L);
correctness;
func Top L -> Element of L equals
"/\"({},L);
correctness;
end;
theorem
for L being lower-bounded antisymmetric non empty RelStr for x being
Element of L holds Bottom L <= x
proof
let L be lower-bounded antisymmetric non empty RelStr;
let x be Element of L;
{} is_<=_than x & ex_sup_of {},L by Th42;
hence thesis by Th30;
end;
theorem
for L being upper-bounded antisymmetric non empty RelStr for x being
Element of L holds x <= Top L
proof
let L be upper-bounded non empty antisymmetric RelStr;
let x be Element of L;
{} is_>=_than x & ex_inf_of {},L by Th43;
hence thesis by Th31;
end;
theorem Th46:
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
proof
let L be non empty RelStr, X,Y be set such that
A1: for x being Element of L holds x is_>=_than X iff x is_>=_than Y;
given a being Element of L such that
A2: X is_<=_than a and
A3: for b being Element of L st X is_<=_than b holds a <= b and
A4: for c being Element of L st X is_<=_than c & for b being Element of
L st X is_<=_than b holds c <= b holds c = a;
take a;
thus Y is_<=_than a by A1,A2;
thus for b being Element of L st Y is_<=_than b holds a <= b by A1,A3;
let c be Element of L;
assume
A5: Y is_<=_than c;
assume
A6: for b being Element of L st Y is_<=_than b holds c <= b;
A7: for b being Element of L st X is_<=_than b holds c <= b by A1,A6;
X is_<=_than c by A1,A5;
hence thesis by A4,A7;
end;
theorem Th47:
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)
proof
let L be non empty RelStr, X,Y be set;
assume
A1: ex_sup_of X,L;
assume
A2: for x being Element of L holds x is_>=_than X iff x is_>=_than Y;
A3: now
let b be Element of L;
assume Y is_<=_than b;
then X is_<=_than b by A2;
hence "\/"(X,L) <= b by A1,Def9;
end;
X is_<=_than "\/"(X,L) by A1,Def9;
then
A4: Y is_<=_than "\/"(X,L) by A2;
ex_sup_of Y,L by A1,A2,Th46;
hence thesis by A4,A3,Def9;
end;
theorem Th48:
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
proof
let L be non empty RelStr, X,Y be set such that
A1: for x being Element of L holds x is_<=_than X iff x is_<=_than Y;
given a being Element of L such that
A2: X is_>=_than a and
A3: for b being Element of L st X is_>=_than b holds a >= b and
A4: for c being Element of L st X is_>=_than c & for b being Element of
L st X is_>=_than b holds c >= b holds c = a;
take a;
thus Y is_>=_than a by A1,A2;
thus for b being Element of L st Y is_>=_than b holds a >= b by A1,A3;
let c be Element of L;
assume
A5: Y is_>=_than c;
assume
A6: for b being Element of L st Y is_>=_than b holds c >= b;
A7: for b being Element of L st X is_>=_than b holds c >= b by A1,A6;
X is_>=_than c by A1,A5;
hence thesis by A4,A7;
end;
theorem Th49:
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)
proof
let L be non empty RelStr, X,Y be set;
assume
A1: ex_inf_of X,L;
assume
A2: for x being Element of L holds x is_<=_than X iff x is_<=_than Y;
A3: now
let b be Element of L;
assume Y is_>=_than b;
then X is_>=_than b by A2;
hence "/\"(X,L) >= b by A1,Def10;
end;
X is_>=_than "/\"(X,L) by A1,Def10;
then
A4: Y is_>=_than "/\"(X,L) by A2;
ex_inf_of Y,L by A1,A2,Th48;
hence thesis by A4,A3,Def10;
end;
theorem Th50:
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)
proof
let L be non empty RelStr, X be set;
set Y = X /\ the carrier of L;
( for x being Element of L holds x is_<=_than X iff x is_<=_than Y)& for
x being Element of L holds x is_>=_than X iff x is_>=_than Y by Th5;
hence thesis by Th46,Th48;
end;
theorem
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)
proof
let L be non empty RelStr, X be set;
set Y = X /\ the carrier of L;
assume
A1: ex_sup_of X,L or ex_sup_of Y,L;
for x being Element of L holds x is_>=_than X iff x is_>=_than Y by Th5;
hence thesis by A1,Th47;
end;
theorem
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)
proof
let L be non empty RelStr, X be set;
set Y = X /\ the carrier of L;
assume
A1: ex_inf_of X,L or ex_inf_of Y,L;
for x being Element of L holds x is_<=_than X iff x is_<=_than Y by Th5;
hence thesis by A1,Th49;
end;
theorem
for L being non empty RelStr st for X being Subset of L holds
ex_sup_of X,L holds L is complete
proof
let L be non empty RelStr such that
A1: for X being Subset of L holds ex_sup_of X,L;
let X be set;
take "\/"(X,L);
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
ex_sup_of Y,L by A1;
then ex_sup_of X,L by Th50;
hence thesis by Def9;
end;
theorem
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
proof
let L be non empty Poset;
hereby
defpred P[set] means $1 is non empty implies ex_sup_of $1,L;
assume
A1: L is with_suprema;
let X be finite non empty Subset of L;
A2: for x,Y being set st x in X & Y c= X & P[Y] holds P[Y \/ {x}]
proof
let x,Y be set such that
A3: x in X and
Y c= X and
A4: Y is non empty implies ex_sup_of Y,L;
reconsider z = x as Element of L by A3;
assume Y \/ {x} is non empty;
per cases;
suppose
Y is empty;
then Y \/ {x} = {z};
hence thesis by Th38;
end;
suppose
A5: Y is non empty;
thus ex_sup_of Y \/ {x}, L
proof
take a = "\/"(Y,L)"\/"z;
A6: Y is_<=_than "\/"(Y,L) by A4,Def9;
A7: ex_sup_of {"\/"(Y,L),z},L by A1,Th20;
then z <= a by Th18;
then
A8: {x} is_<=_than a by Th7;
"\/" (Y,L) <= a by A7,Th18;
then
A9: Y is_<=_than a by A6,Th11;
hence Y \/ {x} is_<=_than a by A8,Th10;
hereby
let b be Element of L;
assume
A10: Y \/ {x} is_<=_than b;
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_<=_than b by A10;
then
A11: "\/"(Y,L) <= b by A4,A5,Def9;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z <= b by A10;
hence b >= a by A7,A11,Th18;
end;
let c be Element of L such that
A12: Y \/ {x} is_<=_than c and
A13: for b being Element of L st Y \/ {x} is_<=_than b holds b >= c;
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_<=_than c by A12;
then
A14: "\/"(Y,L) <= c by A4,A5,Def9;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z <= c by A12;
then
A15: c >= a by A7,A14,Th18;
a >= c by A9,A8,A13,Th10;
hence thesis by A15,ORDERS_2:2;
end;
end;
end;
A16: P[{}];
A17: X is finite;
P[X] from FINSET_1:sch 2(A17,A16,A2);
hence ex_sup_of X,L;
end;
assume for X being finite non empty Subset of L holds ex_sup_of X,L;
then for a,b being Element of L holds ex_sup_of {a,b},L;
hence thesis by Th20;
end;
theorem
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
proof
let L be non empty Poset;
hereby
defpred P[set] means $1 is non empty implies ex_inf_of $1,L;
assume
A1: L is with_infima;
let X be finite non empty Subset of L;
A2: for x,Y being set st x in X & Y c= X & P[Y] holds P[Y \/ {x}]
proof
let x,Y be set such that
A3: x in X and
Y c= X and
A4: Y is non empty implies ex_inf_of Y,L;
reconsider z = x as Element of L by A3;
assume Y \/ {x} is non empty;
per cases;
suppose
Y is empty;
then Y \/ {x} = {z};
hence thesis by Th38;
end;
suppose
A5: Y is non empty;
thus ex_inf_of Y \/ {x}, L
proof
take a = "/\"(Y,L)"/\"z;
A6: Y is_>=_than "/\"(Y,L) by A4,Def10;
A7: ex_inf_of {"/\"(Y,L),z},L by A1,Th21;
then z >= a by Th19;
then
A8: {x} is_>=_than a by Th7;
"/\"(Y,L) >= a by A7,Th19;
then
A9: Y is_>=_than a by A6,Th12;
hence Y \/ {x} is_>=_than a by A8,Th10;
hereby
let b be Element of L;
assume
A10: Y \/ {x} is_>=_than b;
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_>=_than b by A10;
then
A11: "/\"(Y,L) >= b by A4,A5,Def10;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z >= b by A10;
hence b <= a by A7,A11,Th19;
end;
let c be Element of L such that
A12: Y \/ {x} is_>=_than c and
A13: for b being Element of L st Y \/ {x} is_>=_than b holds b <= c;
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_>=_than c by A12;
then
A14: "/\"(Y,L) >= c by A4,A5,Def10;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z >= c by A12;
then
A15: c <= a by A7,A14,Th19;
a <= c by A9,A8,A13,Th10;
hence thesis by A15,ORDERS_2:2;
end;
end;
end;
A16: P[{}];
A17: X is finite;
P[X] from FINSET_1:sch 2(A17,A16,A2);
hence ex_inf_of X,L;
end;
assume for X being finite non empty Subset of L holds ex_inf_of X,L;
then for a,b being Element of L holds ex_inf_of {a,b},L;
hence thesis by Th21;
end;
begin
definition
let L be RelStr;
mode SubRelStr of L -> RelStr means
:Def13:
the carrier of it c= the carrier
of L & the InternalRel of it c= the InternalRel of L;
existence;
end;
definition
let L be RelStr;
let S be SubRelStr of L;
attr S is full means
:Def14:
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;
existence
proof
set S = RelStr(#the carrier of L, the InternalRel of L#);
reconsider S as SubRelStr of L by Def13;
take S;
thus S is strict;
thus the InternalRel of S = (the InternalRel of L)|_2 the carrier of S by
XBOOLE_1:28;
end;
end;
registration
let L be non empty RelStr;
cluster non empty full strict for SubRelStr of L;
existence
proof
set S = RelStr(#the carrier of L, the InternalRel of L#);
reconsider S as SubRelStr of L by Def13;
take S;
thus the carrier of S is non empty;
thus the InternalRel of S = (the InternalRel of L)|_2 the carrier of S by
XBOOLE_1:28;
thus thesis;
end;
end;
theorem Th56:
for L being RelStr, X being Subset of L holds RelStr(#X, (the
InternalRel of L)|_2 X#) is full SubRelStr of L
by XBOOLE_1:17,Def13,Def14;
theorem Th57:
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
proof
let L be RelStr, S1,S2 be full SubRelStr of L;
the InternalRel of S1 = (the InternalRel of L)|_2 the carrier of S1 by Def14;
hence thesis by Def14;
end;
definition
let L be RelStr;
let X be Subset of L;
func subrelstr X -> full strict SubRelStr of L means
the carrier of it = X;
uniqueness by Th57;
existence
proof
RelStr(#X, (the InternalRel of L)|_2 X#) is full SubRelStr of L by Th56;
hence thesis;
end;
end;
theorem Th58:
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
proof
let L be non empty RelStr, S be non empty SubRelStr of L;
let x be Element of S;
x in the carrier of S & the carrier of S c= the carrier of L by Def13;
hence thesis;
end;
theorem Th59:
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
proof
let L be RelStr, S be SubRelStr of L;
let a,b be Element of L, x,y be Element of S such that
A1: x = a & y = b;
A2: the InternalRel of S c= the InternalRel of L by Def13;
assume [x,y] in the InternalRel of S;
hence [a,b] in the InternalRel of L by A1,A2;
end;
theorem Th60:
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
proof
let L be RelStr, S be full SubRelStr of L;
let a,b be Element of L, x,y be Element of S such that
A1: x = a & y = b;
assume
A2: [a,b] in the InternalRel of L;
A3: the InternalRel of S = (the InternalRel of L)|_2 the carrier of S by Def14;
assume x in the carrier of S;
then [x,y] in [:the carrier of S,the carrier of S:] by ZFMISC_1:87;
hence [x,y] in the InternalRel of S by A1,A3,A2,XBOOLE_0:def 4;
end;
theorem Th61:
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)
proof
let L be non empty RelStr, S be non empty full SubRelStr of L,X be set;
let a be Element of L;
let x be Element of S;
assume
A1: x = a;
hereby
assume
A2: a is_<=_than X;
thus x is_<=_than X
proof
let y be Element of S;
reconsider b = y as Element of L by Th58;
assume y in X;
then a <= b by A2;
hence thesis by A1,Th60;
end;
end;
assume
A3: a is_>=_than X;
let y be Element of S;
reconsider b = y as Element of L by Th58;
assume y in X;
then a >= b by A3;
hence thesis by A1,Th60;
end;
theorem Th62:
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)
by Th59;
registration
let L be reflexive RelStr;
cluster -> reflexive for full SubRelStr of L;
coherence
proof
let S be full SubRelStr of L;
let x be object;
assume
A1: x in the carrier of S;
then
A2: [x,x] in [:the carrier of S, the carrier of S :] by ZFMISC_1:87;
the carrier of S c= the carrier of L & the InternalRel of L
is_reflexive_in the carrier of L by Def13,ORDERS_2:def 2;
then
A3: [x,x] in the InternalRel of L by A1;
the InternalRel of S = (the InternalRel of L)|_2 the carrier of S by Def14;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
end;
registration
let L be transitive RelStr;
cluster -> transitive for full SubRelStr of L;
coherence
proof
let S be full SubRelStr of L;
let x,y,z be Element of S;
assume that
A1: x <= y and
A2: y <= z;
A3: the carrier of S c= the carrier of L by Def13;
[y,z] in the InternalRel of S by A2;
then
A4: z in the carrier of S by ZFMISC_1:87;
A5: [x,y] in the InternalRel of S by A1;
then
A6: x in the carrier of S by ZFMISC_1:87;
y in the carrier of S by A5,ZFMISC_1:87;
then reconsider a = x, b = y, c = z as Element of L by A6,A4,A3;
a <= b & b <= c by A1,A2,Th59;
hence thesis by A6,Th60,ORDERS_2:3;
end;
end;
registration
let L be antisymmetric RelStr;
cluster -> antisymmetric for full SubRelStr of L;
coherence
proof
let S be full SubRelStr of L;
let x,y be Element of S;
assume that
A1: x <= y and
A2: y <= x;
A3: the carrier of S c= the carrier of L by Def13;
[x,y] in the InternalRel of S by A1;
then x in the carrier of S & y in the carrier of S by ZFMISC_1:87;
then reconsider a = x, b = y as Element of L by A3;
a <= b & b <= a by A1,A2,Th59;
hence thesis by ORDERS_2:2;
end;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is meet-inheriting means
:Def16:
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
:Def17:
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
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
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;
coherence
proof
let S be SubRelStr of L;
assume
A1: for X being Subset of S st ex_inf_of X,L holds "/\"(X,L) in the
carrier of S;
let x,y be Element of L;
assume x in the carrier of S & y in the carrier of S;
then {x,y} c= the carrier of S by ZFMISC_1:32;
hence thesis by A1;
end;
cluster sups-inheriting -> join-inheriting for SubRelStr of L;
coherence
proof
let S be SubRelStr of L;
assume
A2: for X being Subset of S st ex_sup_of X,L holds "\/"(X,L) in the
carrier of S;
let x,y be Element of L;
assume x in the carrier of S & y in the carrier of S;
then {x,y} c= the carrier of S by ZFMISC_1:32;
hence thesis by A2;
end;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting sups-inheriting non empty full strict for
SubRelStr of L;
existence
proof
the carrier of L c= the carrier of L & (the InternalRel of L)|_2 the
carrier of L = the InternalRel of L by XBOOLE_1:28;
then reconsider
S = RelStr(#the carrier of L, the InternalRel of L#) as non
empty full strict SubRelStr of L by Th56;
take S;
thus S is infs-inheriting;
thus S is sups-inheriting;
thus thesis;
end;
end;
theorem Th63:
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)
proof
let L be non empty transitive RelStr;
let S be non empty full SubRelStr of L;
let X be Subset of S;
assume that
A1: ex_inf_of X,L and
A2: "/\"(X,L) in the carrier of S;
reconsider a = "/\"(X,L) as Element of S by A2;
A3: now
"/\"(X,L) is_<=_than X by A1,Def10;
hence a is_<=_than X by Th61;
let b be Element of S;
reconsider b9 = b as Element of L by Th58;
assume b is_<=_than X;
then b9 is_<=_than X by Th62;
then b9 <= "/\"(X,L) by A1,Def10;
hence b <= a by Th60;
end;
consider a9 being Element of L such that
A4: X is_>=_than a9 and
A5: for b being Element of L st X is_>=_than b holds b <= a9 and
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 = a9 by A1;
A6: a9 = "/\"(X,L) by A1,A4,A5,Def10;
thus ex_inf_of X,S
proof
take a;
thus a is_<=_than X & for b being Element of S st b is_<=_than X holds b
<= a by A3;
let c be Element of S;
reconsider c9 = c as Element of L by Th58;
assume X is_>=_than c;
then
A7: X is_>=_than c9 by Th62;
assume for b being Element of S st X is_>=_than b holds b <= c;
then
A8: a <= c by A3;
now
let b be Element of L;
assume X is_>=_than b;
then
A9: b <= a9 by A5;
a9 <= c9 by A6,A8,Th59;
hence b <= c9 by A9,ORDERS_2:3;
end;
hence thesis by A1,A7,Def10;
end;
hence thesis by A3,Def10;
end;
theorem Th64:
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)
proof
let L be non empty transitive RelStr;
let S be non empty full SubRelStr of L;
let X be Subset of S;
assume that
A1: ex_sup_of X,L and
A2: "\/"(X,L) in the carrier of S;
reconsider a = "\/"(X,L) as Element of S by A2;
A3: now
"\/"(X,L) is_>=_than X by A1,Def9;
hence a is_>=_than X by Th61;
let b be Element of S;
reconsider b9 = b as Element of L by Th58;
assume b is_>=_than X;
then b9 is_>=_than X by Th62;
then b9 >= "\/"(X,L) by A1,Def9;
hence b >= a by Th60;
end;
consider a9 being Element of L such that
A4: X is_<=_than a9 and
A5: for b being Element of L st X is_<=_than b holds b >= a9 and
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 = a9 by A1;
A6: a9 = "\/"(X,L) by A1,A4,A5,Def9;
thus ex_sup_of X,S
proof
take a;
thus a is_>=_than X & for b being Element of S st b is_>=_than X holds b
>= a by A3;
let c be Element of S;
reconsider c9 = c as Element of L by Th58;
assume X is_<=_than c;
then
A7: X is_<=_than c9 by Th62;
assume for b being Element of S st X is_<=_than b holds b >= c;
then
A8: a >= c by A3;
now
let b be Element of L;
assume X is_<=_than b;
then
A9: b >= a9 by A5;
a9 >= c9 by A6,A8,Th59;
hence b >= c9 by A9,ORDERS_2:3;
end;
hence thesis by A1,A7,Def9;
end;
hence thesis by A3,Def9;
end;
theorem
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) by
Th63;
theorem
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) by
Th64;
registration
let L be with_infima antisymmetric transitive RelStr;
cluster -> with_infima for non empty meet-inheriting full SubRelStr of L;
coherence
proof
let S be non empty meet-inheriting full SubRelStr of L;
now
let x,y be Element of S;
reconsider a = x, b = y as Element of L by Th58;
A1: ex_inf_of {a,b}, L by Th21;
then "/\"({a,b},L) in the carrier of S by Def16;
hence ex_inf_of {x,y}, S by A1,Th63;
end;
hence thesis by Th21;
end;
end;
registration
let L be with_suprema antisymmetric transitive RelStr;
cluster -> with_suprema for non empty join-inheriting full SubRelStr of L;
coherence
proof
let S be non empty join-inheriting full SubRelStr of L;
now
let x,y be Element of S;
reconsider a = x, b = y as Element of L by Th58;
A1: ex_sup_of {a,b}, L by Th20;
then "\/"({a,b},L) in the carrier of S by Def17;
hence ex_sup_of {x,y}, S by A1,Th64;
end;
hence thesis by Th20;
end;
end;
theorem
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)
proof
let L be complete non empty Poset;
let S be non empty full SubRelStr of L;
let X be Subset of S such that
A1: "/\"(X,L) in the carrier of S;
ex_inf_of X,L by Th17;
hence thesis by A1,Th63;
end;
theorem
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)
proof
let L be complete non empty Poset;
let S be non empty full SubRelStr of L;
let X be Subset of S such that
A1: "\/"(X,L) in the carrier of S;
ex_sup_of X,L by Th17;
hence thesis by A1,Th64;
end;
theorem
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
proof
let L be with_infima Poset;
let S be meet-inheriting non empty full SubRelStr of L;
let x,y be Element of S, a,b be Element of L such that
A1: a = x & b = y;
A2: ex_inf_of {a,b},L by Th21;
then "/\"({x,y},L) in the carrier of S by A1,Def16;
then
A3: "/\"({x,y},S) = "/\"({x,y},L) by A1,A2,Th63;
a"/\"b = inf {a,b} by Th40;
hence thesis by A1,A3,Th40;
end;
theorem
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
proof
let L be with_suprema Poset;
let S be join-inheriting non empty full SubRelStr of L;
let x,y be Element of S, a,b be Element of L such that
A1: a = x & b = y;
A2: ex_sup_of {a,b},L by Th20;
then "\/"({x,y},L) in the carrier of S by A1,Def17;
then
A3: "\/"({x,y},S) = "\/"({x,y},L) by A1,A2,Th64;
a"\/"b = sup {a,b } by Th41;
hence thesis by A1,A3,Th41;
end;