:: Directed Sets, Nets, Ideals, Filters, and Maps
:: by Grzegorz Bancerek
::
:: Received September 12, 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 ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, RELAT_2, FINSET_1,
LATTICE3, TARSKI, LATTICES, YELLOW_0, STRUCT_0, EQREL_1, CAT_1, FUNCT_1,
RELAT_1, SEQM_3, FUNCOP_1, SETFAM_1, ORDINAL2, CARD_FIL, REWRITE1,
ZFMISC_1, ORDERS_1, CARD_1, TREES_2, WAYBEL_0;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, RELAT_2, FINSET_1,
FUNCT_1, RELSET_1, ORDINAL1, NUMBERS, FUNCT_2, FUNCOP_1, ORDERS_1,
DOMAIN_1, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_2, ORDERS_3;
constructors SETFAM_1, DOMAIN_1, LATTICE3, YELLOW_0, ORDERS_3, REALSET1,
RELSET_1, NUMBERS;
registrations XBOOLE_0, RELSET_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3,
YELLOW_0, SUBSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_3, XBOOLE_0;
equalities STRUCT_0, LATTICE3;
expansions TARSKI, LATTICE3, YELLOW_0, ORDERS_3;
theorems TARSKI, ZFMISC_1, ORDERS_2, LATTICE3, FUNCT_2, FUNCOP_1, YELLOW_0,
RELAT_2, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes FINSET_1, XBOOLE_0;
begin :: Directed subsets
definition
let L be RelStr;
let X be Subset of L;
attr X is directed means
:Def1: :: Definition 1.1
for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & x <= z & y <= z;
attr X is filtered means
:Def2: :: Definition 1.1
for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & z <= x & z <= y;
end;
:: Original "directed subset" is equivalent to "non empty directed subset"
:: in our terminology. It is shown bellow.
theorem Th1:
for L being non empty transitive RelStr, X being Subset of L holds
X is non empty directed iff for Y being finite Subset of X
ex x being Element of L st x in X & x is_>=_than Y
proof
let L be non empty transitive RelStr, X be Subset of L;
hereby
assume X is non empty;
then reconsider X9 = X as non empty set;
assume
A1: X is directed;
let Y be finite Subset of X;
defpred P[set] means ex x being Element of L st x in X & x is_>=_than $1;
A2: Y is finite;
set x = the Element of X9;
x in X;
then reconsider x as Element of L;
x is_>=_than {};
then
A3: P[{}];
A4: now
let x,B be set;
assume that
A5: x in Y and B c= Y;
assume P[B];
then consider y being Element of L such that
A6: y in X and
A7: y is_>=_than B;
x in X by A5;
then reconsider x9 = x as Element of L;
consider z being Element of L such that
A8: z in X and
A9: x9 <= z and
A10: y <= z by A1,A5,A6;
thus P[B \/ {x}]
proof
take z;
thus z in X by A8;
let a be Element of L;
reconsider a9 = a as Element of L;
assume a in B \/ {x};
then a9 in B or a9 in {x} by XBOOLE_0:def 3;
then y >= a9 or a9 = x by A7,TARSKI:def 1;
hence thesis by A9,A10,ORDERS_2:3;
end;
end;
thus P[Y] from FINSET_1:sch 2(A2,A3,A4);
end;
assume
A11: for Y being finite Subset of X
ex x being Element of L st x in X & x is_>=_than Y;
{} c= X;
then ex x being Element of L st x in X & x is_>=_than {} by A11;
hence X is non empty;
let x,y be Element of L;
assume that
A12: x in X and
A13: y in X;
{x,y} c= X by A12,A13,ZFMISC_1:32;
then consider z being Element of L such that
A14: z in X and
A15: z is_>=_than {x,y} by A11;
take z;
A16: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence thesis by A14,A15,A16;
end;
:: Original "filtered subset" is equivalent to "non empty filtered subset"
:: in our terminology. It is shown bellow.
theorem Th2:
for L being non empty transitive RelStr, X being Subset of L holds
X is non empty filtered iff for Y being finite Subset of X
ex x being Element of L st x in X & x is_<=_than Y
proof
let L be non empty transitive RelStr, X be Subset of L;
hereby
assume X is non empty;
then reconsider X9 = X as non empty set;
assume
A1: X is filtered;
let Y be finite Subset of X;
defpred P[set] means ex x being Element of L st x in X & x is_<=_than $1;
A2: Y is finite;
set x = the Element of X9;
x in X;
then reconsider x as Element of L;
x is_<=_than {};
then
A3: P[{}];
A4: now
let x,B be set;
assume that
A5: x in Y and B c= Y;
assume P[B];
then consider y being Element of L such that
A6: y in X and
A7: y is_<=_than B;
x in X by A5;
then reconsider x9 = x as Element of L;
consider z being Element of L such that
A8: z in X and
A9: x9 >= z and
A10: y >= z by A1,A5,A6;
thus P[B \/ {x}]
proof
take z;
thus z in X by A8;
let a be Element of L;
reconsider a9 = a as Element of L;
assume a in B \/ {x};
then a9 in B or a9 in {x} by XBOOLE_0:def 3;
then y <= a9 or a9 = x by A7,TARSKI:def 1;
hence thesis by A9,A10,ORDERS_2:3;
end;
end;
thus P[Y] from FINSET_1:sch 2(A2,A3,A4);
end;
assume
A11: for Y being finite Subset of X
ex x being Element of L st x in X & x is_<=_than Y;
{} c= X;
then ex x being Element of L st x in X & x is_<=_than {} by A11;
hence X is non empty;
let x,y be Element of L;
assume that
A12: x in X and
A13: y in X;
{x,y} c= X by A12,A13,ZFMISC_1:32;
then consider z being Element of L such that
A14: z in X and
A15: z is_<=_than {x,y} by A11;
take z;
A16: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence thesis by A14,A15,A16;
end;
registration
let L be RelStr;
cluster empty -> directed filtered for Subset of L;
coherence;
end;
registration
let L be RelStr;
cluster directed filtered for Subset of L;
existence
proof
take {}L;
thus thesis;
end;
end;
theorem Th3:
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 & X1 is directed
holds X2 is directed
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X1 be Subset of L1, X2 be Subset of L2 such that
A2: X1 = X2;
assume
A3: for x,y being Element of L1 st x in X1 & y in X1
ex z being Element of L1 st z in X1 & x <= z & y <= z;
let x,y be Element of L2;
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume that
A4: x in X2 and
A5: y in X2;
consider z9 being Element of L1 such that
A6: z9 in X1 and
A7: x9 <= z9 and
A8: y9 <= z9 by A2,A3,A4,A5;
reconsider z = z9 as Element of L2 by A1;
take z;
thus thesis by A1,A2,A6,A7,A8,YELLOW_0:1;
end;
theorem
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 & X1 is filtered
holds X2 is filtered
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X1 be Subset of L1, X2 be Subset of L2 such that
A2: X1 = X2;
assume
A3: for x,y being Element of L1 st x in X1 & y in X1
ex z being Element of L1 st z in X1 & x >= z & y >= z;
let x,y be Element of L2;
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume that
A4: x in X2 and
A5: y in X2;
consider z9 being Element of L1 such that
A6: z9 in X1 and
A7: x9 >= z9 and
A8: y9 >= z9 by A2,A3,A4,A5;
reconsider z = z9 as Element of L2 by A1;
take z;
thus thesis by A1,A2,A6,A7,A8,YELLOW_0:1;
end;
theorem Th5:
for L being non empty reflexive RelStr, x being Element of L
holds {x} is directed filtered
proof
let L be non empty reflexive RelStr;
let x be Element of L;
set X = {x};
hereby
let z,y be Element of L;
assume that
A1: z in X and
A2: y in X;
take x;
thus x in X & z <= x & y <= x by A1,A2,TARSKI:def 1;
end;
hereby
let z,y be Element of L;
assume that
A3: z in X and
A4: y in X;
take x;
thus x in X & x <= z & x <= y by A3,A4,TARSKI:def 1;
end;
end;
registration
let L be non empty reflexive RelStr;
cluster directed filtered non empty finite for Subset of L;
existence
proof set x = the Element of L;
take {x};
thus thesis by Th5;
end;
end;
registration
let L be with_suprema RelStr;
cluster [#]L -> directed;
coherence
proof
set X = [#]L;
let x,y be Element of L;
assume that x in X and y in X;
ex z being Element of L st x <= z & y <= z &
for z9 being Element of L st x <= z9 & y <= z9 holds z <= z9
by LATTICE3:def 10;
hence thesis;
end;
end;
registration
let L be upper-bounded non empty RelStr;
cluster [#]L -> directed;
coherence
proof
set X = [#]L;
let x,y be Element of L;
assume that x in X and y in X;
consider z being Element of L such that
A1: z is_>=_than X by YELLOW_0:def 5;
take z;
thus thesis by A1;
end;
end;
registration
let L be with_infima RelStr;
cluster [#]L -> filtered;
coherence
proof
set X = [#]L;
let x,y be Element of L such that x in X and y in X;
ex z being Element of L st z <= x & z <= y &
for z9 being Element of L st z9 <= x & z9 <= y holds z9 <= z
by LATTICE3:def 11;
hence thesis;
end;
end;
registration
let L be lower-bounded non empty RelStr;
cluster [#]L -> filtered;
coherence
proof
set X = [#]L;
let x,y be Element of L;
assume that x in X and y in X;
consider z being Element of L such that
A1: z is_<=_than X by YELLOW_0:def 4;
take z;
thus thesis by A1;
end;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is filtered-infs-inheriting means
:Def3:
for X being filtered Subset of S st X <> {} & ex_inf_of X,L
holds "/\"(X,L) in the carrier of S;
attr S is directed-sups-inheriting means
:Def4:
for X being directed Subset of S st X <> {} & ex_sup_of X,L
holds "\/"(X,L) in the carrier of S;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting -> filtered-infs-inheriting for SubRelStr of L;
coherence;
cluster sups-inheriting -> directed-sups-inheriting for SubRelStr of L;
coherence;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting sups-inheriting non empty full strict for
SubRelStr of L;
existence
proof
set S = the infs-inheriting sups-inheriting non empty full strict SubRelStr of
L;
take S;
thus thesis;
end;
end;
theorem
for L being non empty transitive RelStr
for S being filtered-infs-inheriting non empty full SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L
holds ex_inf_of X,S & "/\"(X,S) = "/\"(X,L)
proof
let L be non empty transitive RelStr;
let S be filtered-infs-inheriting non empty full SubRelStr of L;
let X be filtered Subset of S;
assume that
A1: X <> {} and
A2: ex_inf_of X,L;
"/\"(X,L) in the carrier of S by A1,A2,Def3;
hence thesis by A2,YELLOW_0:63;
end;
theorem
for L being non empty transitive RelStr
for S being directed-sups-inheriting non empty full SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L
holds ex_sup_of X,S & "\/"(X,S) = "\/"(X,L)
proof
let L be non empty transitive RelStr;
let S be directed-sups-inheriting non empty full SubRelStr of L;
let X be directed Subset of S;
assume that
A1: X <> {} and
A2: ex_sup_of X,L;
"\/"(X,L) in the carrier of S by A1,A2,Def4;
hence thesis by A2,YELLOW_0:64;
end;
begin :: Nets
definition
let L1,L2 be RelStr;
let f be Function of L1,L2;
attr f is antitone means
for x,y being Element of L1 st x <= y
for a,b being Element of L2 st a = f.x & b = f.y holds a >= b;
end;
:: Definition 1.2
definition
let L be 1-sorted;
struct (RelStr) NetStr over L (# carrier -> set,
InternalRel -> (Relation of the carrier),
mapping -> Function of the carrier, the carrier of L #);
end;
registration
let L be 1-sorted;
let X be non empty set;
let O be Relation of X;
let F be Function of X, the carrier of L;
cluster NetStr(#X,O,F#) -> non empty;
coherence;
end;
definition
let N be RelStr;
attr N is directed means
:Def6:
[#]N is directed;
end;
registration
let L be 1-sorted;
cluster non empty reflexive transitive antisymmetric directed
for strict NetStr over L;
existence
proof set X = the with_suprema Poset;
set M = the Function of the carrier of X, the carrier of L;
take N = NetStr(#the carrier of X, the InternalRel of X, M#);
thus N is non empty;
A1: the InternalRel of N is_reflexive_in the carrier of N by ORDERS_2:def 2;
A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def 3;
the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def 4
;
hence N is reflexive transitive antisymmetric
by A1,A2,ORDERS_2:def 2,def 3,def 4;
A3: the RelStr of N = the RelStr of X;
[#]X = [#]N;
hence [#]N is directed by A3,Th3;
end;
end;
definition
let L be 1-sorted;
mode prenet of L is directed non empty NetStr over L;
end;
definition
let L be 1-sorted;
mode net of L is transitive prenet of L;
end;
definition
let L be non empty 1-sorted;
let N be non empty NetStr over L;
func netmap(N,L) -> Function of N,L equals
the mapping of N;
coherence;
let i be Element of N;
func N.i -> Element of L equals
(the mapping of N).i;
correctness;
end;
definition
let L be non empty RelStr;
let N be non empty NetStr over L;
attr N is monotone means
netmap(N,L) is monotone;
attr N is antitone means
netmap(N,L) is antitone;
end;
definition
let L be non empty 1-sorted;
let N be non empty NetStr over L;
let X be set;
pred N is_eventually_in X means
ex i being Element of N st for j being Element of N st i <= j holds N.j in X;
pred N is_often_in X means
for i being Element of N ex j being Element of N st i <= j & N.j in X;
end;
theorem
for L being non empty 1-sorted, N being non empty NetStr over L
for X,Y being set st X c= Y holds
(N is_eventually_in X implies N is_eventually_in Y) &
(N is_often_in X implies N is_often_in Y)
proof
let L be non empty 1-sorted, N be non empty NetStr over L;
let X,Y be set such that
A1: X c= Y;
hereby
assume N is_eventually_in X;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds N.j in X;
thus N is_eventually_in Y
proof
take i;
let j be Element of N;
assume i <= j;
then N.j in X by A2;
hence thesis by A1;
end;
end;
assume
A3: for i being Element of N ex j being Element of N st i <= j & N.j in X;
let i be Element of N;
consider j being Element of N such that
A4: i <= j and
A5: N.j in X by A3;
take j;
thus thesis by A1,A4,A5;
end;
theorem
for L being non empty 1-sorted, N being non empty NetStr over L
for X being set holds
N is_eventually_in X iff not N is_often_in (the carrier of L) \ X
proof
let L be non empty 1-sorted, N be non empty NetStr over L, X be set;
set Y = (the carrier of L) \ X;
thus N is_eventually_in X implies not N is_often_in Y
proof
given i being Element of N such that
A1: for j being Element of N st i <= j holds N.j in X;
take i;
let j be Element of N;
assume i <= j;
then N.j in X by A1;
hence thesis by XBOOLE_0:def 5;
end;
given i being Element of N such that
A2: for j being Element of N st i <= j holds not N.j in Y;
take i;
let j be Element of N;
assume i <= j;
then not N.j in Y by A2;
hence thesis by XBOOLE_0:def 5;
end;
theorem
for L being non empty 1-sorted, N being non empty NetStr over L
for X being set holds
N is_often_in X iff not N is_eventually_in (the carrier of L) \ X
proof
let L be non empty 1-sorted, N be non empty NetStr over L, X be set;
set Y = (the carrier of L) \ X;
thus N is_often_in X implies not N is_eventually_in Y
proof
assume
A1: for i being Element of N ex j being Element of N st i <= j & N.j in X;
let i be Element of N;
consider j being Element of N such that
A2: i <= j and
A3: N.j in X by A1;
take j;
thus thesis by A2,A3,XBOOLE_0:def 5;
end;
assume
A4: for
i being Element of N ex j being Element of N st i <= j & not N.j in Y;
let i be Element of N;
consider j being Element of N such that
A5: i <= j and
A6: not N.j in Y by A4;
take j;
thus thesis by A5,A6,XBOOLE_0:def 5;
end;
scheme HoldsEventually
{L() -> non empty RelStr, N() -> non empty NetStr over L(), P[set]}:
N() is_eventually_in {N().k where k is Element of N(): P[N().k]} iff
ex i being Element of N() st
for j being Element of N() st i <= j holds P[N().j]
proof
set X = {N().k where k is Element of N(): P[N().k]};
hereby
assume N() is_eventually_in X;
then consider i being Element of N() such that
A1: for j being Element of N() st i <= j holds N().j in X;
take i;
let j be Element of N();
assume i <= j;
then N().j in X by A1;
then ex k being Element of N() st N().j = N().k & P[N().k];
hence P[N().j];
end;
given i being Element of N() such that
A2: for j being Element of N() st i <= j holds P[N().j];
take i;
let j be Element of N();
assume i <= j;
then P[N().j] by A2;
hence thesis;
end;
definition
let L be non empty RelStr;
let N be non empty NetStr over L;
attr N is eventually-directed means
for i being Element of N holds N is_eventually_in
{N.j where j is Element of N: N.i <= N.j};
attr N is eventually-filtered means
for i being Element of N holds N is_eventually_in
{N.j where j is Element of N: N.i >= N.j};
end;
theorem Th11:
for L being non empty RelStr, N being non empty NetStr over L holds
N is eventually-directed iff
for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds N.i <= N.k
proof
let L be non empty RelStr, N be non empty NetStr over L;
A1: now
let i be Element of N;
defpred P[Element of L] means N.i <= $1;
thus N is_eventually_in {N.j where j is Element of N: P[N.j]} iff
ex k being Element of N st for l being Element of N st k <= l holds P[N.l]
from HoldsEventually;
end;
hereby
assume
A2: N is eventually-directed;
let i be Element of N;
N is_eventually_in {N.j where j is Element of N: N.i <= N.j} by A2;
hence ex j being Element of N st
for k being Element of N st j <= k holds N.i <= N.k by A1;
end;
assume
A3: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds N.i <= N.k;
let i be Element of N;
ex j being Element of N st
for k being Element of N st j <= k holds N.i <= N.k by A3;
hence thesis by A1;
end;
theorem Th12:
for L being non empty RelStr, N being non empty NetStr over L holds
N is eventually-filtered iff
for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds N.i >= N.k
proof
let L be non empty RelStr, N be non empty NetStr over L;
A1: now
let i be Element of N;
defpred P[Element of L] means N.i >= $1;
thus N is_eventually_in {N.j where j is Element of N: P[N.j]} iff
ex k being Element of N st for l being Element of N st k <= l holds P[N.l]
from HoldsEventually;
end;
hereby
assume
A2: N is eventually-filtered;
let i be Element of N;
N is_eventually_in {N.j where j is Element of N: N.i >= N.j} by A2;
hence ex j being Element of N st
for k being Element of N st j <= k holds N.i >= N.k by A1;
end;
assume
A3: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds N.i >= N.k;
let i be Element of N;
ex j being Element of N st
for k being Element of N st j <= k holds N.i >= N.k by A3;
hence thesis by A1;
end;
registration
let L be non empty RelStr;
cluster monotone -> eventually-directed for prenet of L;
coherence
proof
let N be prenet of L;
assume
A1: for i,j being Element of N st i <= j
for a,b being Element of L st a = netmap(N,L).i & b = netmap(N,L).j
holds a <= b;
now
let i be Element of N;
take j = i;
let k be Element of N;
assume j <= k;
hence N.i <= N.k by A1;
end;
hence thesis by Th11;
end;
cluster antitone -> eventually-filtered for prenet of L;
coherence
proof
let N be prenet of L;
assume
A2: for i,j being Element of N st i <= j
for a,b being Element of L st a = netmap(N,L).i & b = netmap(N,L).j
holds a >= b;
now
let i be Element of N;
take j = i;
let k be Element of N;
assume j <= k;
hence N.i >= N.k by A2;
end;
hence thesis by Th12;
end;
end;
registration
let L be non empty reflexive RelStr;
cluster monotone antitone strict for prenet of L;
existence
proof set J = the upper-bounded non empty Poset;
set x = the Element of L;
set M = (the carrier of J) --> x;
reconsider M as Function of the carrier of J, the carrier of L;
set N = NetStr(#the carrier of J, the InternalRel of J, M#);
A1: the RelStr of N = the RelStr of J;
[#]J = [#]N;
then [#]N is directed by A1,Th3;
then reconsider N as prenet of L by Def6;
take N;
thus N is monotone
proof
let i,j be Element of N such that i <= j;
let a,b be Element of L;
assume that
A2: a = netmap(N,L).i and
A3: b = netmap(N,L).j;
A4: a = x by A2,FUNCOP_1:7;
x <= x;
hence thesis by A3,A4,FUNCOP_1:7;
end;
thus N is antitone
proof
let i,j be Element of N such that i <= j;
let a,b be Element of L;
assume that
A5: a = netmap(N,L).i and
A6: b = netmap(N,L).j;
A7: a = x by A5,FUNCOP_1:7;
x <= x;
hence thesis by A6,A7,FUNCOP_1:7;
end;
thus thesis;
end;
end;
begin :: Closure by lower elements and finite sups
:: Definition 1.3
definition
let L be RelStr;
let X be Subset of L;
func downarrow X -> Subset of L means
:Def15:
for x being Element of L holds x in it iff
ex y being Element of L st y >= x & y in X;
existence
proof
defpred P[object] means
ex a,y being Element of L st a = $1 & y >= a & y in X;
consider S being set such that
A1: for x being object holds x in S iff x in the carrier of L & P[x]
from XBOOLE_0:sch 1;
S c= the carrier of L
by A1;
then reconsider S as Subset of L;
take S;
let x be Element of L;
hereby
assume x in S;
then ex a,y being Element of L st a = x & y >= a & y in X by A1;
hence ex y being Element of L st y >= x & y in X;
end;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be Subset of L such that
A2: for x being Element of L holds x in S1 iff
ex y being Element of L st y >= x & y in X and
A3: for x being Element of L holds x in S2 iff
ex y being Element of L st y >= x & y in X;
thus S1 c= S2
proof
let x be object;
assume
A4: x in S1;
then reconsider x as Element of L;
ex y being Element of L st y >= x & y in X by A2,A4;
hence thesis by A3;
end;
let x be object;
assume
A5: x in S2;
then reconsider x as Element of L;
ex y being Element of L st y >= x & y in X by A3,A5;
hence thesis by A2;
end;
func uparrow X -> Subset of L means
:Def16:
for x being Element of L holds x in it iff
ex y being Element of L st y <= x & y in X;
existence
proof
defpred P[object] means
ex a,y being Element of L st a = $1 & y <= a & y in X;
consider S being set such that
A6: for x being object holds x in S iff x in the carrier of L & P[x]
from XBOOLE_0:sch 1;
S c= the carrier of L
by A6;
then reconsider S as Subset of L;
take S;
let x be Element of L;
hereby
assume x in S;
then ex a,y being Element of L st a = x & y <= a & y in X by A6;
hence ex y being Element of L st y <= x & y in X;
end;
thus thesis by A6;
end;
correctness
proof
let S1,S2 be Subset of L such that
A7: for x being Element of L holds x in S1 iff
ex y being Element of L st y <= x & y in X and
A8: for x being Element of L holds x in S2 iff
ex y being Element of L st y <= x & y in X;
thus S1 c= S2
proof
let x be object;
assume
A9: x in S1;
then reconsider x as Element of L;
ex y being Element of L st y <= x & y in X by A7,A9;
hence thesis by A8;
end;
let x be object;
assume
A10: x in S2;
then reconsider x as Element of L;
ex y being Element of L st y <= x & y in X by A8,A10;
hence thesis by A7;
end;
end;
theorem Th13:
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
for X being Subset of L1 for Y being Subset of L2
st X = Y holds downarrow X = downarrow Y & uparrow X = uparrow Y
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X be Subset of L1;
let Y be Subset of L2 such that
A2: X = Y;
thus downarrow X c= downarrow Y
proof
let x be object;
assume
A3: x in downarrow X;
then reconsider x as Element of L1;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A4: y >= x and
A5: y in X by A3,Def15;
reconsider y9 = y as Element of L2 by A1;
y9 >= x9 by A1,A4,YELLOW_0:1;
hence thesis by A2,A5,Def15;
end;
thus downarrow Y c= downarrow X
proof
let x be object;
assume
A6: x in downarrow Y;
then reconsider x as Element of L2;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A7: y >= x and
A8: y in Y by A6,Def15;
reconsider y9 = y as Element of L1 by A1;
y9 >= x9 by A1,A7,YELLOW_0:1;
hence thesis by A2,A8,Def15;
end;
thus uparrow X c= uparrow Y
proof
let x be object;
assume
A9: x in uparrow X;
then reconsider x as Element of L1;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A10: y <= x and
A11: y in X by A9,Def16;
reconsider y9 = y as Element of L2 by A1;
y9 <= x9 by A1,A10,YELLOW_0:1;
hence thesis by A2,A11,Def16;
end;
thus uparrow Y c= uparrow X
proof
let x be object;
assume
A12: x in uparrow Y;
then reconsider x as Element of L2;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A13: y <= x and
A14: y in Y by A12,Def16;
reconsider y9 = y as Element of L1 by A1;
y9 <= x9 by A1,A13,YELLOW_0:1;
hence thesis by A2,A14,Def16;
end;
end;
theorem Th14:
for L being non empty RelStr, X being Subset of L holds downarrow X =
{x where x is Element of L: ex y being Element of L st x <= y & y in X}
proof
let L be non empty RelStr, X be Subset of L;
set Y={x where x is Element of L: ex y being Element of L st x <=
y & y in X};
hereby
let x be object;
assume
A1: x in downarrow X;
then reconsider y = x as Element of L;
ex z being Element of L st z >= y & z in X by A1,Def15;
hence x in Y;
end;
let x be object;
assume x in Y;
then ex a being Element of L st a = x &
ex y being Element of L st a <= y & y in X;
hence thesis by Def15;
end;
theorem Th15:
for L being non empty RelStr, X being Subset of L holds uparrow X =
{x where x is Element of L: ex y being Element of L st x >= y & y in X}
proof
let L be non empty RelStr, X be Subset of L;
set Y={x where x is Element of L: ex y being Element of L st x >=
y & y in X};
hereby
let x be object;
assume
A1: x in uparrow X;
then reconsider y = x as Element of L;
ex z being Element of L st z <= y & z in X by A1,Def16;
hence x in Y;
end;
let x be object;
assume x in Y;
then ex a being Element of L st a = x &
ex y being Element of L st a >= y & y in X;
hence thesis by Def16;
end;
registration
let L be non empty reflexive RelStr;
let X be non empty Subset of L;
cluster downarrow X -> non empty;
coherence
proof set x = the Element of X;
reconsider x9 = x as Element of L;
x9 <= x9;
hence thesis by Def15;
end;
cluster uparrow X -> non empty;
coherence
proof set x = the Element of X;
reconsider x9 = x as Element of L;
x9 <= x9;
hence thesis by Def16;
end;
end;
theorem Th16:
for L being reflexive RelStr, X being Subset of L holds
X c= downarrow X & X c= uparrow X
proof
let L be reflexive RelStr, X be Subset of L;
A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
hereby
let x be object;
assume
A2: x in X;
then reconsider y = x as Element of L;
[y,y] in the InternalRel of L by A1,A2,RELAT_2:def 1;
then y <= y by ORDERS_2:def 5;
hence x in downarrow X by A2,Def15;
end;
let x be object;
assume
A3: x in X;
then reconsider y = x as Element of L;
[y,y] in the InternalRel of L by A1,A3,RELAT_2:def 1;
then y <= y by ORDERS_2:def 5;
hence thesis by A3,Def16;
end;
definition
let L be non empty RelStr;
let x be Element of L;
func downarrow x -> Subset of L equals :: Definition 1.3 (iii)
downarrow {x};
correctness;
func uparrow x -> Subset of L equals :: Definition 1.3 (iv)
uparrow {x};
correctness;
end;
theorem Th17:
for L being non empty RelStr, x,y being Element of L
holds y in downarrow x iff y <= x
proof
let L be non empty RelStr, x,y be Element of L;
A1: downarrow x = {z where z is Element of L:
ex v being Element of L st z <= v & v in {x}} by Th14;
then y in downarrow x iff ex z being Element of L st y = z &
ex v being Element of L st z <= v & v in {x};
hence y in downarrow x implies y <= x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
hence thesis by A1;
end;
theorem Th18:
for L being non empty RelStr, x,y being Element of L
holds y in uparrow x iff x <= y
proof
let L be non empty RelStr, x,y be Element of L;
A1: uparrow x = {z where z is Element of L:
ex v being Element of L st z >= v & v in {x}} by Th15;
then y in uparrow x iff ex z being Element of L st y = z &
ex v being Element of L st z >= v & v in {x};
hence y in uparrow x implies y >= x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
hence thesis by A1;
end;
theorem
for L being non empty reflexive antisymmetric RelStr
for x,y being Element of L st downarrow x = downarrow y holds x = y
proof
let L be non empty reflexive antisymmetric RelStr;
let x,y be Element of L;
reconsider x9 = x, y9 = y as Element of L;
A1: x9 <= x9;
A2: y9 <= y9;
assume
A3: downarrow x = downarrow y;
then
A4: y in downarrow x by A2,Th17;
x in downarrow y by A1,A3,Th17;
then
A5: x9 <= y9 by Th17;
x9 >= y9 by A4,Th17;
hence thesis by A5,ORDERS_2:2;
end;
theorem
for L being non empty reflexive antisymmetric RelStr
for x,y being Element of L st uparrow x = uparrow y holds x = y
proof
let L be non empty reflexive antisymmetric RelStr;
let x,y be Element of L;
reconsider x9 = x, y9 = y as Element of L;
A1: x9 <= x9;
A2: y9 <= y9;
assume
A3: uparrow x = uparrow y;
then
A4: y in uparrow x by A2,Th18;
A5: x in uparrow y by A1,A3,Th18;
A6: x9 <= y9 by A4,Th18;
x9 >= y9 by A5,Th18;
hence thesis by A6,ORDERS_2:2;
end;
theorem Th21:
for L being non empty transitive RelStr for x,y being Element of L st x <= y
holds downarrow x c= downarrow y
proof
let L be non empty transitive RelStr;
let x,y be Element of L such that
A1: x <= y;
let z be object;
assume
A2: z in downarrow x;
then reconsider z as Element of L;
z <= x by A2,Th17;
then z <= y by A1,ORDERS_2:3;
hence thesis by Th17;
end;
theorem Th22:
for L being non empty transitive RelStr for x,y being Element of L st x <= y
holds uparrow y c= uparrow x
proof
let L be non empty transitive RelStr;
let x,y be Element of L such that
A1: x <= y;
let z be object;
assume
A2: z in uparrow y;
then reconsider z as Element of L;
y <= z by A2,Th18;
then x <= z by A1,ORDERS_2:3;
hence thesis by Th18;
end;
registration
let L be non empty reflexive RelStr;
let x be Element of L;
cluster downarrow x -> non empty directed;
coherence
proof reconsider x9 = x as Element of L;
thus downarrow x is non empty;
let z,y be Element of L;
assume that
A1: z in downarrow x and
A2: y in downarrow x;
take x9;
x9 <= x9;
hence x9 in downarrow x & z <= x9 & y <= x9 by A1,A2,Th17;
end;
cluster uparrow x -> non empty filtered;
coherence
proof reconsider x9 = x as Element of L;
thus uparrow x is non empty;
let z,y be Element of L;
assume that
A3: z in uparrow x and
A4: y in uparrow x;
take x9;
x9 <= x9;
hence x9 in uparrow x & x9 <= z & x9 <= y by A3,A4,Th18;
end;
end;
definition
let L be RelStr;
let X be Subset of L;
attr X is lower means
:Def19: :: Definition 1.3 (v)
for x,y being Element of L st x in X & y <= x holds y in X;
attr X is upper means
:Def20: :: Definition 1.3 (vi)
for x,y being Element of L st x in X & x <= y holds y in X;
end;
registration
let L be RelStr;
cluster lower upper for Subset of L;
existence
proof the carrier of L c= the carrier of L;
then reconsider S = the carrier of L as Subset of L;
take S;
thus S is lower;
let x be Element of L;
thus thesis;
end;
end;
theorem Th23:
for L being RelStr, X being Subset of L holds X is lower iff downarrow X c= X
proof
let L be RelStr, X be Subset of L;
hereby
assume
A1: X is lower;
thus downarrow X c= X
proof
let x be object;
assume
A2: x in downarrow X;
then reconsider x9 = x as Element of L;
ex y being Element of L st x9 <= y & y in X by A2,Def15;
hence thesis by A1;
end;
end;
assume
A3: downarrow X c= X;
let x,y be Element of L;
assume that
A4: x in X and
A5: y <= x;
y in downarrow X by A4,A5,Def15;
hence thesis by A3;
end;
theorem Th24:
for L being RelStr, X being Subset of L holds X is upper iff uparrow X c= X
proof
let L be RelStr, X be Subset of L;
hereby
assume
A1: X is upper;
thus uparrow X c= X
proof
let x be object;
assume
A2: x in uparrow X;
then reconsider x9 = x as Element of L;
ex y being Element of L st x9 >= y & y in X by A2,Def16;
hence thesis by A1;
end;
end;
assume
A3: uparrow X c= X;
let x,y be Element of L;
assume that
A4: x in X and
A5: y >= x;
y in uparrow X by A4,A5,Def16;
hence thesis by A3;
end;
theorem
for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 holds
(X1 is lower implies X2 is lower) & (X1 is upper implies X2 is upper)
proof
let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
let X1 be Subset of L1, X2 be Subset of L2;
assume
A2: X1 = X2;
hereby
assume
A3: X1 is lower;
A4: downarrow X1 = downarrow X2 by A1,A2,Th13;
downarrow X1 c= X1 by A3,Th23;
hence X2 is lower by A2,A4,Th23;
end;
assume
A5: X1 is upper;
A6: uparrow X1 = uparrow X2 by A1,A2,Th13;
uparrow X1 c= X1 by A5,Th24;
hence thesis by A2,A6,Th24;
end;
theorem
for L being RelStr, A being Subset-Family of L st
for X being Subset of L st X in A holds X is lower
holds union A is lower Subset of L
proof
let L be RelStr, A be Subset-Family of L such that
A1: for X being Subset of L st X in A holds X is lower;
reconsider A as Subset-Family of L;
reconsider X = union A as Subset of L;
X is lower
proof
let x,y be Element of L;
assume x in X;
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
reconsider Y as Subset of L by A3;
A4: Y is lower by A1,A3;
assume y <= x;
then y in Y by A2,A4;
hence thesis by A3,TARSKI:def 4;
end;
hence thesis;
end;
theorem Th27:
for L being RelStr, X,Y being Subset of L st X is lower & Y is lower
holds X /\ Y is lower & X \/ Y is lower
proof
let L be RelStr;
let X,Y be Subset of L such that
A1: for x,y being Element of L st x in X & y <= x holds y in X and
A2: for x,y being Element of L st x in Y & y <= x holds y in Y;
hereby
let x,y be Element of L;
assume
A3: x in X /\ Y;
then
A4: x in X by XBOOLE_0:def 4;
A5: x in Y by A3,XBOOLE_0:def 4;
assume
A6: y <= x;
then
A7: y in X by A1,A4;
y in Y by A2,A5,A6;
hence y in X /\ Y by A7,XBOOLE_0:def 4;
end;
let x,y be Element of L;
assume x in X \/ Y;
then
A8: x in X or x in Y by XBOOLE_0:def 3;
assume y <= x;
then y in X or y in Y by A1,A2,A8;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for L being RelStr, A being Subset-Family of L st
for X being Subset of L st X in A holds X is upper
holds union A is upper Subset of L
proof
let L be RelStr, A be Subset-Family of L such that
A1: for X being Subset of L st X in A holds X is upper;
reconsider A as Subset-Family of L;
reconsider X = union A as Subset of L;
X is upper
proof
let x,y be Element of L;
assume x in X;
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
reconsider Y as Subset of L by A3;
A4: Y is upper by A1,A3;
assume y >= x;
then y in Y by A2,A4;
hence thesis by A3,TARSKI:def 4;
end;
hence thesis;
end;
theorem Th29:
for L being RelStr, X,Y being Subset of L st X is upper & Y is upper
holds X /\ Y is upper & X \/ Y is upper
proof
let L be RelStr;
let X,Y be Subset of L such that
A1: for x,y being Element of L st x in X & y >= x holds y in X and
A2: for x,y being Element of L st x in Y & y >= x holds y in Y;
hereby
let x,y be Element of L;
assume
A3: x in X /\ Y;
then
A4: x in X by XBOOLE_0:def 4;
A5: x in Y by A3,XBOOLE_0:def 4;
assume
A6: y >= x;
then
A7: y in X by A1,A4;
y in Y by A2,A5,A6;
hence y in X /\ Y by A7,XBOOLE_0:def 4;
end;
let x,y be Element of L;
assume x in X \/ Y;
then
A8: x in X or x in Y by XBOOLE_0:def 3;
assume y >= x;
then y in X or y in Y by A1,A2,A8;
hence thesis by XBOOLE_0:def 3;
end;
registration
let L be non empty transitive RelStr;
let X be Subset of L;
cluster downarrow X -> lower;
coherence
proof
let y,z be Element of L;
assume y in downarrow X;
then consider x being Element of L such that
A1: y <= x and
A2: x in X by Def15;
assume z <= y;
then z <= x by A1,ORDERS_2:3;
hence thesis by A2,Def15;
end;
cluster uparrow X -> upper;
coherence
proof
let y,z be Element of L;
assume y in uparrow X;
then consider x being Element of L such that
A3: y >= x and
A4: x in X by Def16;
assume z >= y;
then z >= x by A3,ORDERS_2:3;
hence thesis by A4,Def16;
end;
end;
registration
let L be non empty transitive RelStr;
let x be Element of L;
cluster downarrow x -> lower;
coherence;
cluster uparrow x -> upper;
coherence;
end;
registration
let L be non empty RelStr;
cluster [#]L -> lower upper;
coherence;
end;
registration
let L be non empty RelStr;
cluster non empty lower upper for Subset of L;
existence
proof
take [#]L;
thus thesis;
end;
end;
registration
let L be non empty reflexive transitive RelStr;
cluster non empty lower directed for Subset of L;
existence
proof set x = the Element of L;
take downarrow x;
thus thesis;
end;
cluster non empty upper filtered for Subset of L;
existence
proof set x = the Element of L;
take uparrow x;
thus thesis;
end;
end;
registration
let L be with_infima with_suprema Poset;
cluster non empty directed filtered lower upper for Subset of L;
existence
proof
take [#]L;
thus thesis;
end;
end;
theorem Th30:
for L being non empty transitive reflexive RelStr, X be Subset of L holds
X is directed iff downarrow X is directed
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
thus X is directed implies downarrow X is directed
proof
assume
A1: for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & x <= z & y <= z;
let x,y be Element of L;
assume that
A2: x in downarrow X and
A3: y in downarrow X;
consider x9 being Element of L such that
A4: x <= x9 and
A5: x9 in X by A2,Def15;
consider y9 being Element of L such that
A6: y <= y9 and
A7: y9 in X by A3,Def15;
consider z being Element of L such that
A8: z in X and
A9: x9 <= z and
A10: y9 <= z by A1,A5,A7;
take z;
z <= z;
hence z in downarrow X by A8,Def15;
thus thesis by A4,A6,A9,A10,ORDERS_2:3;
end;
set Y = downarrow X;
assume
A11: for x,y being Element of L st x in Y & y in Y
ex z being Element of L st z in Y & x <= z & y <= z;
let x,y be Element of L;
assume that
A12: x in X and
A13: y in X;
A14: x <= x;
A15: y <= y;
A16: x in Y by A12,A14,Def15;
y in Y by A13,A15,Def15;
then consider z being Element of L such that
A17: z in Y and
A18: x <= z and
A19: y <= z by A11,A16;
consider z9 being Element of L such that
A20: z <= z9 and
A21: z9 in X by A17,Def15;
take z9;
thus z9 in X by A21;
thus thesis by A18,A19,A20,ORDERS_2:3;
end;
registration
let L be non empty transitive reflexive RelStr;
let X be directed Subset of L;
cluster downarrow X -> directed;
coherence by Th30;
end;
theorem Th31:
for L being non empty transitive reflexive RelStr, X be Subset of L
for x be Element of L holds x is_>=_than X iff x is_>=_than downarrow X
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
let x be Element of L;
thus x is_>=_than X implies x is_>=_than downarrow X
proof
assume
A1: for y being Element of L st y in X holds x >= y;
let y be Element of L;
assume y in downarrow X;
then consider z being Element of L such that
A2: y <= z and
A3: z in X by Def15;
x >= z by A1,A3;
hence thesis by A2,ORDERS_2:3;
end;
assume
A4: for y being Element of L st y in downarrow X holds x >= y;
let y be Element of L;
assume
A5: y in X;
y <= y;
then y in downarrow X by A5,Def15;
hence thesis by A4;
end;
theorem Th32:
for L being non empty transitive reflexive RelStr, X be Subset of L holds
ex_sup_of X,L iff ex_sup_of downarrow X,L
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
for x being Element of L holds x is_>=_than X iff x is_>=_than downarrow X
by Th31;
hence thesis by YELLOW_0:46;
end;
theorem Th33:
for L being non empty transitive reflexive RelStr, X be Subset of L
st ex_sup_of X,L holds sup X = sup downarrow X
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
for x being Element of L holds x is_>=_than X iff x is_>=_than downarrow X
by Th31;
hence thesis by YELLOW_0:47;
end;
theorem
for L being non empty Poset, x being Element of L holds
ex_sup_of downarrow x, L & sup downarrow x = x
proof
let L be non empty Poset, x be Element of L;
ex_sup_of {x}, L by YELLOW_0:38;
hence ex_sup_of downarrow x, L by Th32;
thus sup downarrow x = sup {x} by Th33,YELLOW_0:38
.= x by YELLOW_0:39;
end;
theorem Th35:
for L being non empty transitive reflexive RelStr, X be Subset of L holds
X is filtered iff uparrow X is filtered
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
thus X is filtered implies uparrow X is filtered
proof
assume
A1: for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & x >= z & y >= z;
let x,y be Element of L;
assume that
A2: x in uparrow X and
A3: y in uparrow X;
consider x9 being Element of L such that
A4: x >= x9 and
A5: x9 in X by A2,Def16;
consider y9 being Element of L such that
A6: y >= y9 and
A7: y9 in X by A3,Def16;
consider z being Element of L such that
A8: z in X and
A9: x9 >= z and
A10: y9 >= z by A1,A5,A7;
take z;
z >= z by ORDERS_2:1;
hence z in uparrow X by A8,Def16;
thus thesis by A4,A6,A9,A10,ORDERS_2:3;
end;
set Y = uparrow X;
assume
A11: for x,y being Element of L st x in Y & y in Y
ex z being Element of L st z in Y & x >= z & y >= z;
let x,y be Element of L;
assume that
A12: x in X and
A13: y in X;
A14: x >= x by ORDERS_2:1;
A15: y >= y by ORDERS_2:1;
A16: x in Y by A12,A14,Def16;
y in Y by A13,A15,Def16;
then consider z being Element of L such that
A17: z in Y and
A18: x >= z and
A19: y >= z by A11,A16;
consider z9 being Element of L such that
A20: z >= z9 and
A21: z9 in X by A17,Def16;
take z9;
thus z9 in X by A21;
thus thesis by A18,A19,A20,ORDERS_2:3;
end;
registration
let L be non empty transitive reflexive RelStr;
let X be filtered Subset of L;
cluster uparrow X -> filtered;
coherence by Th35;
end;
theorem Th36:
for L being non empty transitive reflexive RelStr, X be Subset of L
for x be Element of L holds x is_<=_than X iff x is_<=_than uparrow X
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
let x be Element of L;
thus x is_<=_than X implies x is_<=_than uparrow X
proof
assume
A1: for y being Element of L st y in X holds x <= y;
let y be Element of L;
assume y in uparrow X;
then consider z being Element of L such that
A2: y >= z and
A3: z in X by Def16;
x <= z by A1,A3;
hence thesis by A2,ORDERS_2:3;
end;
assume
A4: for y being Element of L st y in uparrow X holds x <= y;
let y be Element of L;
assume
A5: y in X;
y <= y;
then y in uparrow X by A5,Def16;
hence thesis by A4;
end;
theorem Th37:
for L being non empty transitive reflexive RelStr, X be Subset of L holds
ex_inf_of X,L iff ex_inf_of uparrow X,L
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
for x being Element of L holds x is_<=_than X iff x is_<=_than uparrow X
by Th36;
hence thesis by YELLOW_0:48;
end;
theorem Th38:
for L being non empty transitive reflexive RelStr, X be Subset of L
st ex_inf_of X,L holds inf X = inf uparrow X
proof
let L be non empty transitive reflexive RelStr, X be Subset of L;
for x being Element of L holds x is_<=_than X iff x is_<=_than uparrow X
by Th36;
hence thesis by YELLOW_0:49;
end;
theorem
for L being non empty Poset, x being Element of L holds
ex_inf_of uparrow x, L & inf uparrow x = x
proof
let L be non empty Poset, x be Element of L;
ex_inf_of {x}, L by YELLOW_0:38;
hence ex_inf_of uparrow x, L by Th37;
thus inf uparrow x = inf {x} by Th38,YELLOW_0:38
.= x by YELLOW_0:39;
end;
begin :: Ideals and filters
definition
let L be non empty reflexive transitive RelStr;
mode Ideal of L is directed lower non empty Subset of L;
:: Definition 1.3 (vii)
mode Filter of L is filtered upper non empty Subset of L;
:: Definition 1.3 (viii)
end;
theorem Th40:
for L being with_suprema antisymmetric RelStr, X being lower Subset of L holds
X is directed iff for x,y being Element of L st x in X & y in X holds x"\/"
y in X
proof
let L be with_suprema antisymmetric RelStr, X be lower Subset of L;
thus X is directed implies
for x,y being Element of L st x in X & y in X holds x"\/"y in X
proof
assume
A1: for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & x <= z & y <= z;
let x,y be Element of L;
assume that
A2: x in X and
A3: y in X;
consider z being Element of L such that
A4: z in X and
A5: x <= z and
A6: y <= z by A1,A2,A3;
x"\/"y <= z by A5,A6,YELLOW_0:22;
hence thesis by A4,Def19;
end;
assume
A7: for x,y being Element of L st x in X & y in X holds x"\/"y in X;
let x,y be Element of L;
assume that
A8: x in X and
A9: y in X;
A10: x <= x"\/"y by YELLOW_0:22;
y <= x"\/"y by YELLOW_0:22;
hence thesis by A7,A8,A9,A10;
end;
theorem Th41:
for L being with_infima antisymmetric RelStr, X being upper Subset of L holds
X is filtered iff for x,y being Element of L st x in X & y in X holds x"/\"
y in X
proof
let L be with_infima antisymmetric RelStr, X be upper Subset of L;
thus X is filtered implies
for x,y being Element of L st x in X & y in X holds x"/\"y in X
proof
assume
A1: for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & x >= z & y >= z;
let x,y be Element of L;
assume that
A2: x in X and
A3: y in X;
consider z being Element of L such that
A4: z in X and
A5: x >= z and
A6: y >= z by A1,A2,A3;
x"/\"y >= z by A5,A6,YELLOW_0:23;
hence thesis by A4,Def20;
end;
assume
A7: for x,y being Element of L st x in X & y in X holds x"/\"y in X;
let x,y be Element of L;
assume that
A8: x in X and
A9: y in X;
A10: x >= x"/\"y by YELLOW_0:23;
y >= x"/\"y by YELLOW_0:23;
hence thesis by A7,A8,A9,A10;
end;
theorem Th42:
for L being with_suprema Poset for X being non empty lower Subset of L holds
X is directed iff for Y being finite Subset of X st Y <> {} holds "\/"
(Y,L) in X
proof
let L be with_suprema Poset;
let X be non empty lower Subset of L;
thus X is directed implies
for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in X
proof
assume
A1: X is directed;
let Y be finite Subset of X such that
A2: Y <> {};
consider z being Element of L such that
A3: z in X and
A4: Y is_<=_than z by A1,Th1;
Y c= the carrier of L by XBOOLE_1:1;
then ex_sup_of Y,L by A2,YELLOW_0:54;
then "\/"(Y,L) <= z by A4,YELLOW_0:30;
hence thesis by A3,Def19;
end;
assume
A5: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in X;
set x = the Element of X;
reconsider x as Element of L;
now
let Y be finite Subset of X;
per cases;
suppose Y = {};
then x is_>=_than Y;
hence ex x being Element of L st x in X & x is_>=_than Y;
end;
suppose
A6: Y <> {};
Y c= the carrier of L by XBOOLE_1:1;
then ex_sup_of Y,L by A6,YELLOW_0:54;
then "\/"(Y,L) is_>=_than Y by YELLOW_0:30;
hence ex x being Element of L st x in X & x is_>=_than Y by A5,A6;
end;
end;
hence thesis by Th1;
end;
theorem Th43:
for L being with_infima Poset for X being non empty upper Subset of L holds
X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\"
(Y,L) in X
proof
let L be with_infima Poset, X be non empty upper Subset of L;
thus X is filtered implies
for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in X
proof
assume
A1: X is filtered;
let Y be finite Subset of X such that
A2: Y <> {};
consider z being Element of L such that
A3: z in X and
A4: Y is_>=_than z by A1,Th2;
Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A2,YELLOW_0:55;
then "/\"(Y,L) >= z by A4,YELLOW_0:31;
hence thesis by A3,Def20;
end;
assume
A5: for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in X;
set x = the Element of X;
reconsider x as Element of L;
now
let Y be finite Subset of X;
per cases;
suppose Y = {};
then x is_<=_than Y;
hence ex x being Element of L st x in X & x is_<=_than Y;
end;
suppose
A6: Y <> {};
Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A6,YELLOW_0:55;
then "/\"(Y,L) is_<=_than Y by YELLOW_0:31;
hence ex x being Element of L st x in X & x is_<=_than Y by A5,A6;
end;
end;
hence thesis by Th2;
end;
theorem
for L being non empty antisymmetric RelStr
st L is with_suprema or L is with_infima for X,Y being Subset of L
st X is lower directed & Y is lower directed holds X /\ Y is directed
proof
let L be non empty antisymmetric RelStr such that
A1: L is with_suprema or L is with_infima;
let X,Y be Subset of L such that
A2: X is lower directed and
A3: Y is lower directed;
A4: X /\ Y is lower by A2,A3,Th27;
per cases by A1;
suppose
A5: L is with_suprema;
now
let x,y be Element of L;
assume that
A6: x in X /\ Y and
A7: y in X /\ Y;
A8: x in X by A6,XBOOLE_0:def 4;
A9: x in Y by A6,XBOOLE_0:def 4;
A10: y in X by A7,XBOOLE_0:def 4;
A11: y in Y by A7,XBOOLE_0:def 4;
A12: x"\/"y in X by A2,A5,A8,A10,Th40;
x"\/"y in Y by A3,A5,A9,A11,Th40;
hence x"\/"y in X /\ Y by A12,XBOOLE_0:def 4;
end;
hence thesis by A4,A5,Th40;
end;
suppose
A13: L is with_infima;
let x,y be Element of L;
assume that
A14: x in X /\ Y and
A15: y in X /\ Y;
A16: x in X by A14,XBOOLE_0:def 4;
A17: x in Y by A14,XBOOLE_0:def 4;
A18: y in X by A15,XBOOLE_0:def 4;
A19: y in Y by A15,XBOOLE_0:def 4;
consider zx being Element of L such that
A20: zx in X and
A21: x <= zx and
A22: y <= zx by A2,A16,A18;
consider zy being Element of L such that
A23: zy in Y and
A24: x <= zy and
A25: y <= zy by A3,A17,A19;
take z = zx"/\"zy;
A26: z <= zx by A13,YELLOW_0:23;
A27: z <= zy by A13,YELLOW_0:23;
A28: z in X by A2,A20,A26;
z in Y by A3,A23,A27;
hence z in X /\ Y by A28,XBOOLE_0:def 4;
thus thesis by A13,A21,A22,A24,A25,YELLOW_0:23;
end;
end;
theorem
for L being non empty antisymmetric RelStr
st L is with_suprema or L is with_infima for X,Y being Subset of L
st X is upper filtered & Y is upper filtered holds X /\ Y is filtered
proof
let L be non empty antisymmetric RelStr such that
A1: L is with_suprema or L is with_infima;
let X,Y be Subset of L such that
A2: X is upper filtered and
A3: Y is upper filtered;
A4: X /\ Y is upper by A2,A3,Th29;
per cases by A1;
suppose
A5: L is with_infima;
now
let x,y be Element of L;
assume that
A6: x in X /\ Y and
A7: y in X /\ Y;
A8: x in X by A6,XBOOLE_0:def 4;
A9: x in Y by A6,XBOOLE_0:def 4;
A10: y in X by A7,XBOOLE_0:def 4;
A11: y in Y by A7,XBOOLE_0:def 4;
A12: x"/\"y in X by A2,A5,A8,A10,Th41;
x"/\"y in Y by A3,A5,A9,A11,Th41;
hence x"/\"y in X /\ Y by A12,XBOOLE_0:def 4;
end;
hence thesis by A4,A5,Th41;
end;
suppose
A13: L is with_suprema;
let x,y be Element of L;
assume that
A14: x in X /\ Y and
A15: y in X /\ Y;
A16: x in X by A14,XBOOLE_0:def 4;
A17: x in Y by A14,XBOOLE_0:def 4;
A18: y in X by A15,XBOOLE_0:def 4;
A19: y in Y by A15,XBOOLE_0:def 4;
consider zx being Element of L such that
A20: zx in X and
A21: x >= zx and
A22: y >= zx by A2,A16,A18;
consider zy being Element of L such that
A23: zy in Y and
A24: x >= zy and
A25: y >= zy by A3,A17,A19;
take z = zx"\/"zy;
A26: z >= zx by A13,YELLOW_0:22;
A27: z >= zy by A13,YELLOW_0:22;
A28: z in X by A2,A20,A26;
z in Y by A3,A23,A27;
hence z in X /\ Y by A28,XBOOLE_0:def 4;
thus thesis by A13,A21,A22,A24,A25,YELLOW_0:22;
end;
end;
theorem
for L being RelStr, A being Subset-Family of L st
(for X being Subset of L st X in A holds X is directed) &
(for X,Y being Subset of L st X in A & Y in A
ex Z being Subset of L st Z in A & X \/ Y c= Z)
for X being Subset of L st X = union A holds X is directed
proof
let L be RelStr, A be Subset-Family of L such that
A1: for X being Subset of L st X in A holds X is directed and
A2: for X,Y being Subset of L st X in A & Y in A
ex Z being Subset of L st Z in A & X \/ Y c= Z;
let Z be Subset of L;
assume
A3: Z = union A;
let x,y be Element of L;
assume x in Z;
then consider X being set such that
A4: x in X and
A5: X in A by A3,TARSKI:def 4;
assume y in Z;
then consider Y being set such that
A6: y in Y and
A7: Y in A by A3,TARSKI:def 4;
reconsider X,Y as Subset of L by A5,A7;
consider W being Subset of L such that
A8: W in A and
A9: X \/ Y c= W by A2,A5,A7;
A10: X c= X \/ Y by XBOOLE_1:7;
A11: Y c= X \/ Y by XBOOLE_1:7;
A12: x in X \/ Y by A4,A10;
A13: y in X \/ Y by A6,A11;
W is directed by A1,A8;
then consider z being Element of L such that
A14: z in W and
A15: x <= z and
A16: y <= z by A9,A12,A13;
take z;
thus thesis by A3,A8,A14,A15,A16,TARSKI:def 4;
end;
theorem
for L being RelStr, A being Subset-Family of L st
(for X being Subset of L st X in A holds X is filtered) &
(for X,Y being Subset of L st X in A & Y in A
ex Z being Subset of L st Z in A & X \/ Y c= Z)
for X being Subset of L st X = union A holds X is filtered
proof
let L be RelStr, A be Subset-Family of L such that
A1: for X being Subset of L st X in A holds X is filtered and
A2: for X,Y being Subset of L st X in A & Y in A
ex Z being Subset of L st Z in A & X \/ Y c= Z;
let Z be Subset of L;
assume
A3: Z = union A;
let x,y be Element of L;
assume x in Z;
then consider X being set such that
A4: x in X and
A5: X in A by A3,TARSKI:def 4;
assume y in Z;
then consider Y being set such that
A6: y in Y and
A7: Y in A by A3,TARSKI:def 4;
reconsider X,Y as Subset of L by A5,A7;
consider W being Subset of L such that
A8: W in A and
A9: X \/ Y c= W by A2,A5,A7;
A10: X c= X \/ Y by XBOOLE_1:7;
A11: Y c= X \/ Y by XBOOLE_1:7;
A12: x in X \/ Y by A4,A10;
A13: y in X \/ Y by A6,A11;
W is filtered by A1,A8;
then consider z being Element of L such that
A14: z in W and
A15: x >= z and
A16: y >= z by A9,A12,A13;
take z;
thus thesis by A3,A8,A14,A15,A16,TARSKI:def 4;
end;
definition
let L be non empty reflexive transitive RelStr;
let I be Ideal of L;
attr I is principal means
ex x being Element of L st x in I & x is_>=_than I;
end;
definition
let L be non empty reflexive transitive RelStr;
let F be Filter of L;
attr F is principal means
ex x being Element of L st x in F & x is_<=_than F;
end;
theorem
for L being non empty reflexive transitive RelStr, I being Ideal of L holds
I is principal iff ex x being Element of L st I = downarrow x
proof
let L be non empty reflexive transitive RelStr, I be Ideal of L;
thus I is principal implies ex x being Element of L st I = downarrow x
proof
given x being Element of L such that
A1: x in I and
A2: x is_>=_than I;
take x;
thus I c= downarrow x
by A2,Th17;
let z be object;
assume
A3: z in downarrow x;
then reconsider z as Element of L;
z <= x by A3,Th17;
hence thesis by A1,Def19;
end;
given x being Element of L such that
A4: I = downarrow x;
take x;
x <= x;
hence x in I by A4,Th17;
let y be Element of L;
thus thesis by A4,Th17;
end;
theorem
for L being non empty reflexive transitive RelStr, F being Filter of L holds
F is principal iff ex x being Element of L st F = uparrow x
proof
let L be non empty reflexive transitive RelStr, I be Filter of L;
thus I is principal implies ex x being Element of L st I = uparrow x
proof
given x being Element of L such that
A1: x in I and
A2: x is_<=_than I;
take x;
thus I c= uparrow x
by A2,Th18;
let z be object;
assume
A3: z in uparrow x;
then reconsider z as Element of L;
z >= x by A3,Th18;
hence thesis by A1,Def20;
end;
given x being Element of L such that
A4: I = uparrow x;
take x;
x <= x;
hence x in I by A4,Th18;
let y be Element of L;
thus thesis by A4,Th18;
end;
definition
let L be non empty reflexive transitive RelStr;
func Ids L -> set equals :: Definition 1.3 (xi)
the set of all X where X is Ideal of L;
correctness;
func Filt L -> set equals :: Definition 1.3 (xi)
the set of all X where X is Filter of L;
correctness;
end;
definition
let L be non empty reflexive transitive RelStr;
func Ids_0 L -> set equals :: Definition 1.3 (xii)
Ids L \/ {{}};
correctness;
func Filt_0 L -> set equals :: Definition 1.3 (xiii)
Filt L \/ {{}};
correctness;
end;
definition
let L be non empty RelStr;
let X be Subset of L;
set D = {"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L};
A1: D c= the carrier of L
proof
let x be object;
assume x in D;
then ex Y being finite Subset of X st x = "\/"(Y,L) & ex_sup_of Y,L;
hence thesis;
end;
func finsups X -> Subset of L equals
{"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L};
correctness by A1;
set D = {"/\"(Y,L) where Y is finite Subset of X: ex_inf_of Y,L};
A2: D c= the carrier of L
proof
let x be object;
assume x in D;
then ex Y being finite Subset of X st x = "/\"(Y,L) & ex_inf_of Y,L;
hence thesis;
end;
func fininfs X -> Subset of L equals
{"/\"(Y,L) where Y is finite Subset of X: ex_inf_of Y,L};
correctness by A2;
end;
registration
let L be non empty antisymmetric lower-bounded RelStr;
let X be Subset of L;
cluster finsups X -> non empty;
coherence
proof
ex_sup_of {},L by YELLOW_0:42;
then "\/"({}X,L) in finsups X;
hence thesis;
end;
end;
registration
let L be non empty antisymmetric upper-bounded RelStr;
let X be Subset of L;
cluster fininfs X -> non empty;
coherence
proof
ex_inf_of {},L by YELLOW_0:43;
then "/\"({}X,L) in fininfs X;
hence thesis;
end;
end;
registration
let L be non empty reflexive antisymmetric RelStr;
let X be non empty Subset of L;
cluster finsups X -> non empty;
coherence
proof set x = the Element of X;
reconsider y = x as Element of L;
reconsider Z = {y} as finite Subset of X by ZFMISC_1:31;
ex_sup_of Z,L by YELLOW_0:38;
then "\/"(Z,L) in finsups X;
hence thesis;
end;
cluster fininfs X -> non empty;
coherence
proof set x = the Element of X;
reconsider y = x as Element of L;
reconsider Z = {y} as finite Subset of X by ZFMISC_1:31;
ex_inf_of Z,L by YELLOW_0:38;
then "/\"(Z,L) in fininfs X;
hence thesis;
end;
end;
theorem Th50:
for L being non empty reflexive antisymmetric RelStr for X being Subset of L
holds X c= finsups X & X c= fininfs X
proof
let L be non empty reflexive antisymmetric RelStr;
let X be Subset of L;
hereby
let x be object;
assume
A1: x in X;
then reconsider y = x as Element of L;
reconsider Y = {x} as finite Subset of X by A1,ZFMISC_1:31;
A2: y = "\/"(Y,L) by YELLOW_0:39;
ex_sup_of {y},L by YELLOW_0:38;
hence x in finsups X by A2;
end;
let x be object;
assume
A3: x in X;
then reconsider y = x as Element of L;
reconsider Y = {x} as finite Subset of X by A3,ZFMISC_1:31;
A4: y = "/\"(Y,L) by YELLOW_0:39;
ex_inf_of {y},L by YELLOW_0:38;
hence x in fininfs X by A4;
end;
theorem Th51:
for L being non empty transitive RelStr for X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
holds F is directed
proof
let L be non empty transitive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F;
let x,y be Element of L;
assume
A4: x in F;
then consider Y1 being finite Subset of X such that
A5: ex_sup_of Y1,L and
A6: x = "\/"(Y1,L) by A2;
assume y in F;
then consider Y2 being finite Subset of X such that
A7: ex_sup_of Y2,L and
A8: y = "\/"(Y2,L) by A2;
take z = "\/"(Y1 \/ Y2, L);
A9: Y1 = {} & Y2 = {} & {} \/ {} = {} or Y1 \/ Y2 <> {};
hence z in F by A3,A4,A6;
ex_sup_of Y1 \/ Y2,L by A1,A5,A9;
hence thesis by A5,A6,A7,A8,XBOOLE_1:7,YELLOW_0:34;
end;
registration
let L be with_suprema Poset;
let X be Subset of L;
cluster finsups X -> directed;
coherence
proof reconsider X as Subset of L;
A1: now
let Y be finite Subset of X;
Y c= the carrier of L by XBOOLE_1:1;
hence Y <> {} implies ex_sup_of Y,L by YELLOW_0:54;
end;
A2: now
let x be Element of L;
assume x in finsups X;
then ex Y being finite Subset of X st x = "\/"(Y,L) & ex_sup_of Y,L;
hence ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L);
end;
now
let Y be finite Subset of X;
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {};
then ex_sup_of Z,L by YELLOW_0:54;
hence "\/"(Y,L) in finsups X;
end;
hence thesis by A1,A2,Th51;
end;
end;
theorem Th52:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
for x being Element of L holds x is_>=_than X iff x is_>=_than F
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F;
let x be Element of L;
thus x is_>=_than X implies x is_>=_than F
proof
assume
A4: x is_>=_than X;
let y be Element of L;
assume y in F;
then consider Y being finite Subset of X such that
A5: ex_sup_of Y,L and
A6: y = "\/"(Y,L) by A2;
x is_>=_than Y by A4;
hence thesis by A5,A6,YELLOW_0:def 9;
end;
assume
A7: x is_>=_than F;
let y be Element of L;
assume y in X;
then
A8: {y} c= X by ZFMISC_1:31;
then
A9: sup {y} in F by A3;
ex_sup_of {y},L by A1,A8;
then
A10: {y} is_<=_than sup {y} by YELLOW_0:def 9;
A11: sup {y} <= x by A7,A9;
y <= sup {y} by A10,YELLOW_0:7;
hence thesis by A11,ORDERS_2:3;
end;
theorem Th53:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
holds ex_sup_of X,L iff ex_sup_of F,L
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F;
for x being Element of L holds x is_>=_than X iff x is_>=_than F
by A1,A2,A3,Th52;
hence thesis by YELLOW_0:46;
end;
theorem Th54:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) &
ex_sup_of X,L holds sup F = sup X
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F;
for x being Element of L holds x is_>=_than X iff x is_>=_than F
by A1,A2,A3,Th52;
hence thesis by YELLOW_0:47;
end;
theorem
for L being with_suprema Poset, X being Subset of L
st ex_sup_of X,L or L is complete holds sup X = sup finsups X
proof
let L be with_suprema Poset, X be Subset of L;
assume ex_sup_of X,L or L is complete;
then
A1: ex_sup_of X,L by YELLOW_0:17;
A2: now
let Y be finite Subset of X;
Y c= the carrier of L by XBOOLE_1:1;
hence Y <> {} implies ex_sup_of Y,L by YELLOW_0:54;
end;
A3: now
let x be Element of L;
assume x in finsups X;
then ex Y being finite Subset of X st x = "\/"(Y,L) & ex_sup_of Y,L;
hence ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L);
end;
now
let Y be finite Subset of X;
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {};
then ex_sup_of Z,L by YELLOW_0:54;
hence "\/"(Y,L) in finsups X;
end;
hence thesis by A1,A2,A3,Th54;
end;
theorem Th56:
for L being non empty transitive RelStr for X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
holds F is filtered
proof
let L be non empty transitive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F;
let x,y be Element of L;
assume
A4: x in F;
then consider Y1 being finite Subset of X such that
A5: ex_inf_of Y1,L and
A6: x = "/\"(Y1,L) by A2;
assume y in F;
then consider Y2 being finite Subset of X such that
A7: ex_inf_of Y2,L and
A8: y = "/\"(Y2,L) by A2;
take z = "/\"(Y1 \/ Y2, L);
A9: Y1 = {} & Y2 = {} & {} \/ {} = {} or Y1 \/ Y2 <> {};
hence z in F by A3,A4,A6;
ex_inf_of Y1 \/ Y2,L by A1,A5,A9;
hence thesis by A5,A6,A7,A8,XBOOLE_1:7,YELLOW_0:35;
end;
registration
let L be with_infima Poset;
let X be Subset of L;
cluster fininfs X -> filtered;
coherence
proof reconsider X as Subset of L;
A1: now
let Y be finite Subset of X;
Y c= the carrier of L by XBOOLE_1:1;
hence Y <> {} implies ex_inf_of Y,L by YELLOW_0:55;
end;
A2: now
let x be Element of L;
assume x in fininfs X;
then ex Y being finite Subset of X st x = "/\"(Y,L) & ex_inf_of Y,L;
hence ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L);
end;
now
let Y be finite Subset of X;
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {};
then ex_inf_of Z,L by YELLOW_0:55;
hence "/\"(Y,L) in fininfs X;
end;
hence thesis by A1,A2,Th56;
end;
end;
theorem Th57:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
for x being Element of L holds x is_<=_than X iff x is_<=_than F
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F;
let x be Element of L;
thus x is_<=_than X implies x is_<=_than F
proof
assume
A4: x is_<=_than X;
let y be Element of L;
assume y in F;
then consider Y being finite Subset of X such that
A5: ex_inf_of Y,L and
A6: y = "/\"(Y,L) by A2;
x is_<=_than Y by A4;
hence x <= y by A5,A6,YELLOW_0:def 10;
end;
assume
A7: x is_<=_than F;
let y be Element of L;
assume y in X;
then
A8: {y} c= X by ZFMISC_1:31;
then
A9: inf {y} in F by A3;
ex_inf_of {y},L by A1,A8;
then
A10: {y} is_>=_than inf {y} by YELLOW_0:def 10;
A11: inf {y} >= x by A7,A9;
y >= inf {y} by A10,YELLOW_0:7;
hence thesis by A11,ORDERS_2:3;
end;
theorem Th58:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
holds ex_inf_of X,L iff ex_inf_of F,L
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F;
for x being Element of L holds x is_<=_than X iff x is_<=_than F
by A1,A2,A3,Th57;
hence thesis by YELLOW_0:48;
end;
theorem Th59:
for L being non empty transitive reflexive RelStr, X,F being Subset of L st
(for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
(for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
(for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) &
ex_inf_of X, L holds inf F = inf X
proof
let L be non empty transitive reflexive RelStr;
let X,F be Subset of L such that
A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and
A2: for x being Element of L st x in F
ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L) and
A3: for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F;
for x being Element of L holds x is_<=_than X iff x is_<=_than F
by A1,A2,A3,Th57;
hence thesis by YELLOW_0:49;
end;
theorem
for L being with_infima Poset, X being Subset of L
st ex_inf_of X,L or L is complete holds inf X = inf fininfs X
proof
let L be with_infima Poset, X be Subset of L;
assume ex_inf_of X,L or L is complete;
then
A1: ex_inf_of X,L by YELLOW_0:17;
A2: now
let Y be finite Subset of X;
Y c= the carrier of L by XBOOLE_1:1;
hence Y <> {} implies ex_inf_of Y,L by YELLOW_0:55;
end;
A3: now
let x be Element of L;
assume x in fininfs X;
then ex Y being finite Subset of X st x = "/\"(Y,L) & ex_inf_of Y,L;
hence ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L);
end;
now
let Y be finite Subset of X;
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {};
then ex_inf_of Z,L by YELLOW_0:55;
hence "/\"(Y,L) in fininfs X;
end;
hence thesis by A1,A2,A3,Th59;
end;
theorem
for L being with_suprema Poset, X being Subset of L holds
X c= downarrow finsups X &
for I being Ideal of L st X c= I holds downarrow finsups X c= I
proof
let L be with_suprema Poset, X be Subset of L;
A1: X c= finsups X by Th50;
finsups X c= downarrow finsups X by Th16;
hence X c= downarrow finsups X by A1;
let I be Ideal of L such that
A2: X c= I;
let x be object;
assume
A3: x in downarrow finsups X;
then reconsider x as Element of L;
consider y being Element of L such that
A4: x <= y and
A5: y in finsups X by A3,Def15;
consider Y being finite Subset of X such that
A6: y = "\/"(Y,L) and
A7: ex_sup_of Y,L by A5;
set i = the Element of I;
reconsider i as Element of L;
A8: ex_sup_of {i}, L by YELLOW_0:38;
A9: sup {i} = i by YELLOW_0:39;
A10: now
assume ex_sup_of {},L;
then "\/"({},L) <= sup {i} by A8,XBOOLE_1:2,YELLOW_0:34;
hence "\/"({},L) in I by A9,Def19;
end;
Y c= I by A2;
then y in I by A6,A7,A10,Th42;
hence thesis by A4,Def19;
end;
theorem
for L being with_infima Poset, X being Subset of L holds
X c= uparrow fininfs X &
for F being Filter of L st X c= F holds uparrow fininfs X c= F
proof
let L be with_infima Poset, X be Subset of L;
A1: X c= fininfs X by Th50;
fininfs X c= uparrow fininfs X by Th16;
hence X c= uparrow fininfs X by A1;
let I be Filter of L such that
A2: X c= I;
let x be object;
assume
A3: x in uparrow fininfs X;
then reconsider x as Element of L;
consider y being Element of L such that
A4: x >= y and
A5: y in fininfs X by A3,Def16;
consider Y being finite Subset of X such that
A6: y = "/\"(Y,L) and
A7: ex_inf_of Y,L by A5;
set i = the Element of I;
reconsider i as Element of L;
A8: ex_inf_of {i}, L by YELLOW_0:38;
A9: inf {i} = i by YELLOW_0:39;
A10: now
assume ex_inf_of {},L;
then "/\"({},L) >= inf {i} by A8,XBOOLE_1:2,YELLOW_0:35;
hence "/\"({},L) in I by A9,Def20;
end;
Y c= I by A2;
then y in I by A6,A7,A10,Th43;
hence thesis by A4,Def20;
end;
begin :: Chains
definition
let L be non empty RelStr;
attr L is connected means
:Def29:
for x,y being Element of L holds x <= y or y <= x;
end;
registration
cluster trivial -> connected for non empty reflexive RelStr;
coherence
proof
let L be non empty reflexive RelStr;
assume
A1: for x,y being Element of L holds x = y;
let z1,z2 be Element of L;
z1 = z2 by A1;
hence thesis by ORDERS_2:1;
end;
end;
registration
cluster connected for non empty Poset;
existence
proof set O = the Order of {0};
take L = RelStr(#{0},O#);
let x,y be Element of L;
A1: x = 0 by TARSKI:def 1;
y = 0 by TARSKI:def 1;
hence thesis by A1,ORDERS_2:1;
end;
end;
definition
mode Chain is connected non empty Poset;
end;
registration
let L be Chain;
cluster L~ -> connected;
coherence
proof
let x,y be Element of L~;
A1: (~x)~ = ~x;
A2: (~y)~ = ~y;
~x <= ~y or ~x >= ~y by Def29;
hence thesis by A1,A2,LATTICE3:9;
end;
end;
begin :: Semilattices
definition
mode Semilattice is with_infima Poset;
mode sup-Semilattice is with_suprema Poset;
mode LATTICE is with_infima with_suprema Poset;
end;
theorem
for L being Semilattice for X being upper non empty Subset of L holds
X is Filter of L iff subrelstr X is meet-inheriting
proof
let L be Semilattice, X be upper non empty Subset of L;
set S = subrelstr X;
A1: the carrier of S = X by YELLOW_0:def 15;
hereby
assume
A2: X is Filter of L;
thus S is meet-inheriting
proof
let x,y be Element of L;
assume that
A3: x in the carrier of S and
A4: y in the carrier of S and
A5: ex_inf_of {x,y},L;
consider z being Element of L such that
A6: z in X and
A7: x >= z and
A8: y >= z by A1,A2,A3,A4,Def2;
z is_<=_than {x,y} by A7,A8,YELLOW_0:8;
then z <= inf {x,y} by A5,YELLOW_0:def 10;
hence thesis by A1,A6,Def20;
end;
end;
assume
A9: 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;
X is filtered
proof
let x,y be Element of L;
assume that
A10: x in X and
A11: y in X;
take z = inf {x,y};
A12: z = x "/\" y by YELLOW_0:40;
ex_inf_of {x,y},L by YELLOW_0:21;
hence z in X & z <= x & z <= y by A1,A9,A10,A11,A12,YELLOW_0:19;
end;
hence thesis;
end;
theorem
for L being sup-Semilattice for X being lower non empty Subset of L holds
X is Ideal of L iff subrelstr X is join-inheriting
proof
let L be sup-Semilattice, X be lower non empty Subset of L;
set S = subrelstr X;
A1: the carrier of S = X by YELLOW_0:def 15;
hereby
assume
A2: X is Ideal of L;
thus S is join-inheriting
proof
let x,y be Element of L;
assume that
A3: x in the carrier of S and
A4: y in the carrier of S and
A5: ex_sup_of {x,y},L;
consider z being Element of L such that
A6: z in X and
A7: x <= z and
A8: y <= z by A1,A2,A3,A4,Def1;
z is_>=_than {x,y} by A7,A8,YELLOW_0:8;
then z >= sup {x,y} by A5,YELLOW_0:def 9;
hence thesis by A1,A6,Def19;
end;
end;
assume
A9: 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;
X is directed
proof
let x,y be Element of L;
assume that
A10: x in X and
A11: y in X;
take z = sup {x,y};
A12: z = x "\/" y by YELLOW_0:41;
ex_sup_of {x,y},L by YELLOW_0:20;
hence z in X & x <= z & y <= z by A1,A9,A10,A11,A12,YELLOW_0:18;
end;
hence thesis;
end;
begin :: Maps
definition
let S,T be non empty RelStr;
let f be Function of S,T;
let X be Subset of S;
pred f preserves_inf_of X means
ex_inf_of X,S implies ex_inf_of f.:X,T & inf (f.:X) = f.inf X;
pred f preserves_sup_of X means
ex_sup_of X,S implies ex_sup_of f.:X,T & sup (f.:X) = f.sup X;
end;
theorem
for S1,S2, T1,T2 being non empty RelStr st
the RelStr of S1 = the RelStr of T1 & the RelStr of S2 = the RelStr of T2
for f being Function of S1,S2, g being Function of T1,T2 st f = g
for X being Subset of S1, Y being Subset of T1 st X = Y holds
(f preserves_sup_of X implies g preserves_sup_of Y) &
(f preserves_inf_of X implies g preserves_inf_of Y)
proof
let S1,S2, T1,T2 be non empty RelStr such that
A1: the RelStr of S1 = the RelStr of T1 and
A2: the RelStr of S2 = the RelStr of T2;
let f be Function of S1,S2, g be Function of T1,T2 such that
A3: f = g;
let X be Subset of S1, Y be Subset of T1 such that
A4: X = Y;
thus f preserves_sup_of X implies g preserves_sup_of Y
proof
assume
A5: ex_sup_of X,S1 implies ex_sup_of f.:X,S2 & sup (f.:X) = f.sup X;
assume
A6: ex_sup_of Y,T1;
hence ex_sup_of g.:Y,T2 by A1,A2,A3,A4,A5,YELLOW_0:14;
sup (f.:X) = sup (g.: Y) by A1,A2,A3,A4,A5,A6,YELLOW_0:14,26;
hence thesis by A1,A3,A4,A5,A6,YELLOW_0:14,26;
end;
assume
A7: ex_inf_of X,S1 implies ex_inf_of f.:X,S2 & inf (f.:X) = f.inf X;
assume
A8: ex_inf_of Y,T1;
hence ex_inf_of g.:Y,T2 by A1,A2,A3,A4,A7,YELLOW_0:14;
inf (f.:X) = inf (g.:Y) by A1,A2,A3,A4,A7,A8,YELLOW_0:14,27;
hence thesis by A1,A3,A4,A7,A8,YELLOW_0:14,27;
end;
definition
let L1,L2 be non empty RelStr;
let f be Function of L1,L2;
attr f is infs-preserving means
for X being Subset of L1 holds f preserves_inf_of X;
attr f is sups-preserving means
for X being Subset of L1 holds f preserves_sup_of X;
attr f is meet-preserving means
for x,y being Element of L1 holds f preserves_inf_of {x,y};
attr f is join-preserving means
for x,y being Element of L1 holds f preserves_sup_of {x,y};
attr f is filtered-infs-preserving means
for X being Subset of L1 st X is non empty filtered
holds f preserves_inf_of X;
attr f is directed-sups-preserving means
for X being Subset of L1 st X is non empty directed
holds f preserves_sup_of X;
end;
registration
let L1,L2 be non empty RelStr;
cluster infs-preserving ->
filtered-infs-preserving meet-preserving for Function of L1,L2;
coherence;
cluster sups-preserving ->
directed-sups-preserving join-preserving for Function of L1,L2;
coherence;
end;
definition
let S,T be RelStr;
let f be Function of S,T;
attr f is isomorphic means
:Def38:
f is one-to-one monotone & ex g being Function
of T,S st g = f" & g is monotone if S is non empty & T is non empty
otherwise S is empty & T is empty;
correctness;
end;
theorem Th66:
for S,T being non empty RelStr, f being Function
of S,T holds f is isomorphic iff
f is one-to-one & rng f = the carrier of T &
for x,y being Element of S holds x <= y iff f.x <= f.y
proof
let S,T be non empty RelStr;
let f be Function of S,T;
hereby
assume
A1: f is isomorphic;
hence f is one-to-one by Def38;
consider g being Function of T,S such that
A2: g = f" and
A3: g is monotone by A1,Def38;
A4: f is one-to-one monotone by A1,Def38;
then rng f = dom g by A2,FUNCT_1:33;
hence rng f = the carrier of T by FUNCT_2:def 1;
let x,y be Element of S;
thus x <= y implies f.x <= f.y by A4;
assume
A5: f.x <= f.y;
A6: g.(f.x) = x by A2,A4,FUNCT_2:26;
g.(f.y) = y by A2,A4,FUNCT_2:26;
hence x <= y by A3,A5,A6;
end;
assume that
A7: f is one-to-one and
A8: rng f = the carrier of T and
A9: for x,y being Element of S holds x <= y iff f.x <= f.y;
per cases;
case S is non empty & T is non empty;
thus f is one-to-one by A7;
thus for x,y being Element of S st x <= y
for a,b being Element of T st a = f.x & b = f.y holds a <= b by A9;
reconsider g = f" as Function of T,S by A7,A8,FUNCT_2:25;
take g;
thus g = f";
let x,y be Element of T;
consider a being object such that
A10: a in dom f and
A11: x = f.a by A8,FUNCT_1:def 3;
consider b being object such that
A12: b in dom f and
A13: y = f.b by A8,FUNCT_1:def 3;
reconsider a,b as Element of S by A10,A12;
A14: g.x = a by A7,A11,FUNCT_2:26;
g.y = b by A7,A13,FUNCT_2:26;
hence thesis by A9,A11,A13,A14;
end;
case S is empty or T is empty;
hence thesis;
end;
end;
registration
let S,T be non empty RelStr;
cluster isomorphic -> one-to-one monotone for Function of S,T;
coherence by Def38;
end;
theorem
for S,T being non empty RelStr, f being Function of S,T st f is isomorphic
holds f" is Function of T,S & rng (f") = the carrier of S
proof
let S,T be non empty RelStr, f be Function of S,T;
assume
A1: f is isomorphic;
then
A2: rng f = the carrier of T by Th66;
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: dom (f") = the carrier of T by A1,A2,FUNCT_1:33;
rng (f") = the carrier of S by A1,A3,FUNCT_1:33;
hence thesis by A4,FUNCT_2:1;
end;
theorem
for S,T being non empty RelStr, f being Function of S,T st f is isomorphic
for g being Function of T,S st g = f" holds g is isomorphic
proof
let S,T be non empty RelStr, f be Function of S,T;
assume
A1: f is isomorphic;
then
A2: ex h being Function of T,S st ( h = f")&( h is monotone) by Def38;
let g be Function of T,S;
assume
A3: g = f";
per cases;
case T is non empty & S is non empty;
thus g is one-to-one monotone by A1,A2,A3,FUNCT_1:40;
f" " = f by A1,FUNCT_1:43;
hence thesis by A1,A3;
end;
case T is empty or S is empty;
hence thesis;
end;
end;
theorem Th69:
for S,T being non empty Poset, f being Function of S,T st
for X being Filter of S holds f preserves_inf_of X holds f is monotone
proof
let S,T be non empty Poset, f be Function of S,T;
assume
A1: for X being Filter of S holds f preserves_inf_of X;
let x,y be Element of S;
A2: ex_inf_of {x}, S by YELLOW_0:38;
A3: ex_inf_of {y}, S by YELLOW_0:38;
A4: f preserves_inf_of uparrow x by A1;
A5: f preserves_inf_of uparrow y by A1;
A6: ex_inf_of uparrow x, S by A2,Th37;
A7: ex_inf_of uparrow y, S by A3,Th37;
A8: ex_inf_of f.:uparrow x, T by A4,A6;
A9: ex_inf_of f.:uparrow y, T by A5,A7;
A10: inf (f.:uparrow x) = f.inf uparrow x by A4,A6;
A11: inf (f.:uparrow y) = f.inf uparrow y by A5,A7;
assume x <= y;
then
A12: uparrow y c= uparrow x by Th22;
A13: inf (f.:uparrow x) = f.inf {x} by A10,Th38,YELLOW_0:38;
A14: inf (f.:uparrow y) = f.inf {y} by A11,Th38,YELLOW_0:38;
A15: inf (f.:uparrow x) = f.x by A13,YELLOW_0:39;
inf (f.:uparrow y) = f.y by A14,YELLOW_0:39;
hence thesis by A8,A9,A12,A15,RELAT_1:123,YELLOW_0:35;
end;
theorem
for S,T being non empty Poset, f being Function of S,T st
for X being Filter of S holds f preserves_inf_of X
holds f is filtered-infs-preserving
proof
let S,T be non empty Poset, f be Function of S,T such that
A1: for X being Filter of S holds f preserves_inf_of X;
let X be Subset of S such that
A2: X is non empty filtered and
A3: ex_inf_of X,S;
reconsider Y = X as non empty filtered Subset of S by A2;
uparrow Y is Filter of S;
then
A4: f preserves_inf_of uparrow X by A1;
A5: ex_inf_of uparrow X, S by A3,Th37;
then
A6: ex_inf_of f.:uparrow X,T by A4;
A7: inf (f.:uparrow X) = f.inf uparrow X by A4,A5;
A8: inf uparrow X = inf X by A3,Th38;
A9: f.:X c= f.:uparrow X by Th16,RELAT_1:123;
A10: f.:uparrow X is_>=_than f.inf X by A6,A7,A8,YELLOW_0:31;
A11: f.:X is_>=_than f.inf X
by A9,A10;
A12: now
let b be Element of T;
assume
A13: f.:X is_>=_than b;
f.:uparrow X is_>=_than b
proof
let a be Element of T;
assume a in f.:uparrow X;
then consider x being object such that
x in dom f and
A14: x in uparrow X and
A15: a = f.x by FUNCT_1:def 6;
uparrow X =
{z where z is Element of S: ex y being Element of S st z >= y & y in X}
by Th15;
then consider z being Element of S such that
A16: x = z and
A17: ex y being Element of S st z >= y & y in X by A14;
consider y being Element of S such that
A18: z >= y and
A19: y in X by A17;
A20: f is monotone by A1,Th69;
A21: f.y in f.:X by A19,FUNCT_2:35;
A22: f.z >= f.y by A18,A20;
f.y >= b by A13,A21;
hence thesis by A15,A16,A22,ORDERS_2:3;
end;
hence f.inf X >= b by A6,A7,A8,YELLOW_0:31;
end;
hence ex_inf_of f.:X,T by A11,YELLOW_0:16;
hence thesis by A11,A12,YELLOW_0:def 10;
end;
theorem
for S being Semilattice, T being non empty Poset, f being Function of S,T st
(for X being finite Subset of S holds f preserves_inf_of X) &
(for X being non empty filtered Subset of S holds f preserves_inf_of X)
holds f is infs-preserving
proof
let S be Semilattice, T be non empty Poset, f be Function of S,T such that
A1: for X being finite Subset of S holds f preserves_inf_of X and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X;
let X be Subset of S such that
A3: ex_inf_of X,S;
defpred P[object] means
ex Y being finite Subset of X st ex_inf_of Y, S & $1 = "/\"(Y,S);
consider Z being set such that
A4: for x being object holds x in Z iff x in the carrier of S & P[x]
from XBOOLE_0:sch 1;
Z c= the carrier of S
by A4;
then reconsider Z as Subset of S;
A5: now
let Y be finite Subset of X;
Y is Subset of S by XBOOLE_1:1;
hence Y <> {} implies ex_inf_of Y, S by YELLOW_0:55;
end;
A6: now
let Y be finite Subset of X;
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume Y <> {};
then ex_inf_of Y9, S by YELLOW_0:55;
hence "/\"(Y,S) in Z by A4;
end;
A7: for x being Element of S st x in Z
ex Y being finite Subset of X st ex_inf_of Y,S & x = "/\"(Y,S) by A4;
then
A8: Z is filtered by A5,A6,Th56;
A9: ex_inf_of Z, S by A3,A5,A6,A7,Th58;
Z = {} or Z <> {};
then
A10: f preserves_inf_of Z by A1,A2,A8;
then
A11: ex_inf_of f.:Z,T by A9;
A12: inf (f.:Z) = f.inf Z by A9,A10;
A13: inf Z = inf X by A3,A5,A6,A7,Th59;
X c= Z
proof
let x be object;
assume
A14: x in X;
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x as Element of S by A14;
Y is Subset of S by XBOOLE_1:1;
then
A15: ex_inf_of Y, S by YELLOW_0:55;
x = "/\"(Y,S) by YELLOW_0:39;
hence thesis by A4,A15;
end;
then
A16: f.:X c= f.:Z by RELAT_1:123;
A17: f.:Z is_>=_than f.inf X by A11,A12,A13,YELLOW_0:31;
A18: f.:X is_>=_than f.inf X
by A16,A17;
A19: now
let b be Element of T;
assume
A20: f.:X is_>=_than b;
f.:Z is_>=_than b
proof
let a be Element of T;
assume a in f.:Z;
then consider x being object such that
x in dom f and
A21: x in Z and
A22: a = f.x by FUNCT_1:def 6;
consider Y being finite Subset of X such that
A23: ex_inf_of Y, S and
A24: x = "/\"(Y,S) by A4,A21;
reconsider Y as Subset of S by XBOOLE_1:1;
A25: f.:Y c= f.:X by RELAT_1:123;
A26: f preserves_inf_of Y by A1;
A27: b is_<=_than f.:Y by A20,A25;
A28: a = "/\"(f.:Y,T) by A22,A23,A24,A26;
ex_inf_of f.:Y, T by A23,A26;
hence thesis by A27,A28,YELLOW_0:def 10;
end;
hence f.inf X >= b by A11,A12,A13,YELLOW_0:31;
end;
hence ex_inf_of f.:X,T by A18,YELLOW_0:16;
hence thesis by A18,A19,YELLOW_0:def 10;
end;
theorem Th72:
for S,T being non empty Poset, f being Function of S,T st
for X being Ideal of S holds f preserves_sup_of X holds f is monotone
proof
let S,T be non empty Poset, f be Function of S,T;
assume
A1: for X being Ideal of S holds f preserves_sup_of X;
let x,y be Element of S;
A2: ex_sup_of {x}, S by YELLOW_0:38;
A3: ex_sup_of {y}, S by YELLOW_0:38;
A4: f preserves_sup_of downarrow x by A1;
A5: f preserves_sup_of downarrow y by A1;
A6: ex_sup_of downarrow x, S by A2,Th32;
A7: ex_sup_of downarrow y, S by A3,Th32;
A8: ex_sup_of f.:downarrow x, T by A4,A6;
A9: ex_sup_of f.:downarrow y, T by A5,A7;
A10: sup (f.:downarrow x) = f.sup downarrow x by A4,A6;
A11: sup (f.:downarrow y) = f.sup downarrow y by A5,A7;
assume x <= y;
then
A12: downarrow x c= downarrow y by Th21;
A13: sup (f.:downarrow x) = f.sup {x} by A10,Th33,YELLOW_0:38;
A14: sup (f.:downarrow y) = f.sup {y} by A11,Th33,YELLOW_0:38;
A15: sup (f.:downarrow x) = f.x by A13,YELLOW_0:39;
sup (f.:downarrow y) = f.y by A14,YELLOW_0:39;
hence thesis by A8,A9,A12,A15,RELAT_1:123,YELLOW_0:34;
end;
theorem
for S,T being non empty Poset, f being Function of S,T st
for X being Ideal of S holds f preserves_sup_of X
holds f is directed-sups-preserving
proof
let S,T be non empty Poset, f be Function of S,T such that
A1: for X being Ideal of S holds f preserves_sup_of X;
let X be Subset of S such that
A2: X is non empty directed and
A3: ex_sup_of X,S;
reconsider Y = X as non empty directed Subset of S by A2;
downarrow Y is Ideal of S;
then
A4: f preserves_sup_of downarrow X by A1;
A5: ex_sup_of downarrow X, S by A3,Th32;
then
A6: ex_sup_of f.:downarrow X,T by A4;
A7: sup (f.:downarrow X) = f.sup downarrow X by A4,A5;
A8: sup downarrow X = sup X by A3,Th33;
A9: f.:X c= f.:downarrow X by Th16,RELAT_1:123;
A10: f.:downarrow X is_<=_than f.sup X by A6,A7,A8,YELLOW_0:30;
A11: f.:X is_<=_than f.sup X
by A9,A10;
A12: now
let b be Element of T;
assume
A13: f.:X is_<=_than b;
f.:downarrow X is_<=_than b
proof
let a be Element of T;
assume a in f.:downarrow X;
then consider x being object such that
x in dom f and
A14: x in downarrow X and
A15: a = f.x by FUNCT_1:def 6;
downarrow X =
{z where z is Element of S: ex y being Element of S st z <= y & y in X}
by Th14;
then consider z being Element of S such that
A16: x = z and
A17: ex y being Element of S st z <= y & y in X by A14;
consider y being Element of S such that
A18: z <= y and
A19: y in X by A17;
A20: f is monotone by A1,Th72;
A21: f.y in f.:X by A19,FUNCT_2:35;
A22: f.z <= f.y by A18,A20;
f.y <= b by A13,A21;
hence thesis by A15,A16,A22,ORDERS_2:3;
end;
hence f.sup X <= b by A6,A7,A8,YELLOW_0:30;
end;
hence ex_sup_of f.:X,T by A11,YELLOW_0:15;
hence thesis by A11,A12,YELLOW_0:def 9;
end;
theorem
for S being sup-Semilattice, T being non empty Poset, f being Function
of S,T st (for X being finite Subset of S holds f preserves_sup_of X) &
(for X being non empty directed Subset of S holds f preserves_sup_of X)
holds f is sups-preserving
proof
let S be sup-Semilattice, T be non empty Poset, f be Function of S,T such
that
A1: for X being finite Subset of S holds f preserves_sup_of X and
A2: for X being non empty directed Subset of S holds f preserves_sup_of X;
let X be Subset of S such that
A3: ex_sup_of X,S;
defpred P[object] means
ex Y being finite Subset of X st ex_sup_of Y, S & $1 = "\/"(Y,S);
consider Z being set such that
A4: for x being object holds x in Z iff x in the carrier of S & P[x]
from XBOOLE_0:sch 1;
Z c= the carrier of S
by A4;
then reconsider Z as Subset of S;
A5: now
let Y be finite Subset of X;
Y is Subset of S by XBOOLE_1:1;
hence Y <> {} implies ex_sup_of Y, S by YELLOW_0:54;
end;
A6: now
let Y be finite Subset of X;
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume Y <> {};
then ex_sup_of Y9, S by YELLOW_0:54;
hence "\/"(Y,S) in Z by A4;
end;
A7: for x being Element of S st x in Z
ex Y being finite Subset of X st ex_sup_of Y,S & x = "\/"(Y,S) by A4;
then
A8: Z is directed by A5,A6,Th51;
A9: ex_sup_of Z, S by A3,A5,A6,A7,Th53;
Z = {} or Z <> {};
then
A10: f preserves_sup_of Z by A1,A2,A8;
then
A11: ex_sup_of f.:Z,T by A9;
A12: sup (f.:Z) = f.sup Z by A9,A10;
A13: sup Z = sup X by A3,A5,A6,A7,Th54;
X c= Z
proof
let x be object;
assume
A14: x in X;
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x as Element of S by A14;
Y is Subset of S by XBOOLE_1:1;
then
A15: ex_sup_of Y, S by YELLOW_0:54;
x = "\/"(Y,S) by YELLOW_0:39;
hence thesis by A4,A15;
end;
then
A16: f.:X c= f.:Z by RELAT_1:123;
A17: f.:Z is_<=_than f.sup X by A11,A12,A13,YELLOW_0:30;
A18: f.:X is_<=_than f.sup X
by A16,A17;
A19: now
let b be Element of T;
assume
A20: f.:X is_<=_than b;
f.:Z is_<=_than b
proof
let a be Element of T;
assume a in f.:Z;
then consider x being object such that
x in dom f and
A21: x in Z and
A22: a = f.x by FUNCT_1:def 6;
consider Y being finite Subset of X such that
A23: ex_sup_of Y, S and
A24: x = "\/"(Y,S) by A4,A21;
reconsider Y as Subset of S by XBOOLE_1:1;
A25: f.:Y c= f.:X by RELAT_1:123;
A26: f preserves_sup_of Y by A1;
A27: b is_>=_than f.:Y by A20,A25;
A28: a = "\/"(f.:Y,T) by A22,A23,A24,A26;
ex_sup_of f.:Y, T by A23,A26;
hence thesis by A27,A28,YELLOW_0:def 9;
end;
hence f.sup X <= b by A11,A12,A13,YELLOW_0:30;
end;
hence ex_sup_of f.:X,T by A18,YELLOW_0:15;
hence thesis by A18,A19,YELLOW_0:def 9;
end;
begin :: Complete Semilattice
definition
let L be non empty reflexive RelStr;
attr L is up-complete means
for X being non empty directed Subset of L
ex x being Element of L st x is_>=_than X &
for y being Element of L st y is_>=_than X holds x <= y;
end;
registration
cluster up-complete -> upper-bounded for with_suprema reflexive RelStr;
coherence
proof
let L be with_suprema reflexive RelStr such that
A1: L is up-complete;
[#]L = the carrier of L;
then ex x being Element of L st x is_>=_than the carrier of L &
for y being Element of L st y is_>=_than the carrier of L holds x <= y
by A1;
hence ex x being Element of L st x is_>=_than the carrier of L;
end;
end;
theorem
for L being non empty reflexive antisymmetric RelStr holds L is up-complete
iff for X being non empty directed Subset of L holds ex_sup_of X,L
proof
let L be non empty reflexive antisymmetric RelStr;
hereby
assume
A1: L is up-complete;
let X be non empty directed Subset of L;
consider x being Element of L such that
A2: x is_>=_than X and
A3: for y being Element of L st y is_>=_than X holds x <= y by A1;
thus ex_sup_of X,L
proof
take x;
thus X is_<=_than x &
for b being Element of L st X is_<=_than b holds b >= x by A2,A3;
let c be Element of L;
assume that
A4: X is_<=_than c and
A5: for b being Element of L st X is_<=_than b holds b >= c;
A6: c <= x by A2,A5;
c >= x by A3,A4;
hence thesis by A6,ORDERS_2:2;
end;
end;
assume
A7: for X being non empty directed Subset of L holds ex_sup_of X,L;
let X be non empty directed Subset of L;
ex_sup_of X,L by A7;
then 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;
hence thesis;
end;
definition
let L be non empty reflexive RelStr;
attr L is /\-complete means
for X being non empty Subset of L ex x being Element of L st x is_<=_than X &
for y being Element of L st y is_<=_than X holds x >= y;
end;
theorem Th76:
for L being non empty reflexive antisymmetric RelStr holds L is /\-complete
iff for X being non empty Subset of L holds ex_inf_of X,L
proof
let L be non empty reflexive antisymmetric RelStr;
hereby
assume
A1: L is /\-complete;
let X be non empty Subset of L;
consider x being Element of L such that
A2: x is_<=_than X and
A3: for y being Element of L st y is_<=_than X holds x >= y by A1;
thus ex_inf_of X,L
proof
take x;
thus X is_>=_than x &
for b being Element of L st X is_>=_than b holds b <= x by A2,A3;
let c be Element of L;
assume that
A4: X is_>=_than c and
A5: for b being Element of L st X is_>=_than b holds b <= c;
A6: c <= x by A3,A4;
c >= x by A2,A5;
hence thesis by A6,ORDERS_2:2;
end;
end;
assume
A7: for X being non empty Subset of L holds ex_inf_of X,L;
let X be non empty Subset of L;
ex_inf_of X,L by A7;
then 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;
hence thesis;
end;
registration
cluster complete -> up-complete /\-complete for non empty reflexive RelStr;
coherence
proof
let L be non empty reflexive RelStr such that
A1: L is complete;
thus L is up-complete
by A1;
let X be non empty Subset of L;
set Y = {y where y is Element of L: y is_<=_than X};
consider x being Element of L such that
A2: Y is_<=_than x and
A3: for b being Element of L st Y is_<=_than b holds x <= b by A1;
take x;
thus x is_<=_than X
proof
let y be Element of L such that
A4: y in X;
y is_>=_than Y
proof
let z be Element of L;
assume z in Y;
then ex a being Element of L st z = a & a is_<=_than X;
hence thesis by A4;
end;
hence x <= y by A3;
end;
let y be Element of L;
assume y is_<=_than X;
then y in Y;
hence thesis by A2;
end;
cluster /\-complete -> lower-bounded for non empty reflexive RelStr;
coherence
proof
let L be non empty reflexive RelStr;
assume L is /\-complete;
then ex x being Element of L st x is_<=_than [#]L & for y being Element of L
st y is_<=_than [#]L holds x >= y;
hence ex x being Element of L st x is_<=_than the carrier of L;
end;
cluster up-complete with_suprema lower-bounded -> complete for
non empty Poset;
coherence
proof
let L be non empty Poset;
assume
A5: L is up-complete with_suprema lower-bounded;
then reconsider K = L as with_suprema lower-bounded non empty Poset;
let X be set;
reconsider X9 = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
reconsider A = X9 as Subset of K;
A6: now
let Y be finite Subset of X9;
Y c= the carrier of L by XBOOLE_1:1;
hence Y <> {} implies ex_sup_of Y,L by A5,YELLOW_0:54;
end;
A7: now
let x be Element of L;
assume x in finsups X9;
then ex Y being finite Subset of X9 st x = "\/"(Y,L) & ex_sup_of Y,L;
hence
ex Y being finite Subset of X9 st ex_sup_of Y,L & x = "\/"(Y,L);
end;
A8: now
let Y be finite Subset of X9;
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {};
then ex_sup_of Z,L by A5,YELLOW_0:54;
hence "\/"(Y,L) in finsups X9;
end;
reconsider fX = finsups A as non empty directed Subset of L;
consider x being Element of L such that
A9: fX is_<=_than x and
A10: for y being Element of L st fX is_<=_than y holds x <= y by A5;
take x;
X9 is_<=_than x by A6,A7,A8,A9,Th52;
hence X is_<=_than x by YELLOW_0:5;
let y be Element of L;
assume y is_>=_than X;
then y is_>=_than X9 by YELLOW_0:5;
then y is_>=_than fX by A6,A7,A8,Th52;
hence thesis by A10;
end;
:: cluster up-complete /\-complete upper-bounded -> complete (non empty Poset);
:: to appear in YELLOW_2
end;
registration
cluster /\-complete -> with_infima for
non empty reflexive antisymmetric RelStr;
coherence
proof
let L be non empty reflexive antisymmetric RelStr;
assume L is /\-complete;
then for a,b being Element of L holds ex_inf_of {a,b},L by Th76;
hence thesis by YELLOW_0:21;
end;
end;
registration
cluster /\-complete -> with_suprema
for non empty reflexive antisymmetric upper-bounded RelStr;
coherence
proof
let L be non empty reflexive antisymmetric upper-bounded RelStr such that
A1: L is /\-complete;
now
let a,b be Element of L;
set X = {x where x is Element of L: x >= a & x >= b};
X c= the carrier of L
proof
let x be object;
assume x in X;
then ex z being Element of L st x = z & z >= a & z >= b;
hence thesis;
end;
then reconsider X as Subset of L;
A2: Top L >= a by YELLOW_0:45;
Top L >= b by YELLOW_0:45;
then Top L in X by A2;
then ex_inf_of X,L by A1,Th76;
then consider c being Element of L such that
A3: c is_<=_than X and
A4: for d being Element of L st d is_<=_than X holds d <= c and
for e being Element of L st e is_<=_than X &
for d being Element of L st d is_<=_than X holds d <= e
holds e = c;
A5: c is_>=_than {a,b}
proof
let x be Element of L;
assume
A6: x in {a,b};
x is_<=_than X
proof
let y be Element of L;
assume y in X;
then ex z being Element of L st y = z & z >= a & z >= b;
hence thesis by A6,TARSKI:def 2;
end;
hence thesis by A4;
end;
now
let y be Element of L;
assume
A7: y is_>=_than {a,b};
then
A8: y >= a by YELLOW_0:8;
y >= b by A7,YELLOW_0:8;
then y in X by A8;
hence c <= y by A3;
end;
hence ex_sup_of {a,b},L by A5,YELLOW_0:15;
end;
hence thesis by YELLOW_0:20;
end;
end;
registration
cluster complete strict for LATTICE;
existence
proof set L = the complete strict LATTICE;
take L;
thus thesis;
end;
end;