:: Directed Sets, Nets, Ideals, Filters, and Maps
:: by Grzegorz Bancerek
::
:: Received September 12, 1996
:: Copyright (c) 1996-2017 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;
begin :: Directed subsets
definition
let L be RelStr;
let X be Subset of L;
attr X is directed means
:: WAYBEL_0:def 1
:: 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
:: WAYBEL_0:def 2
:: 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 :: WAYBEL_0:1
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;
:: Original "filtered subset" is equivalent to "non empty filtered subset"
:: in our terminology. It is shown bellow.
theorem :: WAYBEL_0:2
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;
registration
let L be RelStr;
cluster empty -> directed filtered for Subset of L;
end;
registration
let L be RelStr;
cluster directed filtered for Subset of L;
end;
theorem :: WAYBEL_0:3
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;
theorem :: WAYBEL_0:4
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;
theorem :: WAYBEL_0:5
for L being non empty reflexive RelStr, x being Element of L
holds {x} is directed filtered;
registration
let L be non empty reflexive RelStr;
cluster directed filtered non empty finite for Subset of L;
end;
registration
let L be with_suprema RelStr;
cluster [#]L -> directed;
end;
registration
let L be upper-bounded non empty RelStr;
cluster [#]L -> directed;
end;
registration
let L be with_infima RelStr;
cluster [#]L -> filtered;
end;
registration
let L be lower-bounded non empty RelStr;
cluster [#]L -> filtered;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is filtered-infs-inheriting means
:: WAYBEL_0:def 3
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
:: WAYBEL_0:def 4
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;
cluster sups-inheriting -> directed-sups-inheriting for SubRelStr of L;
end;
registration
let L be non empty RelStr;
cluster infs-inheriting sups-inheriting non empty full strict for
SubRelStr of L;
end;
theorem :: WAYBEL_0:6
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);
theorem :: WAYBEL_0:7
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);
begin :: Nets
definition
let L1,L2 be RelStr;
let f be Function of L1,L2;
attr f is antitone means
:: WAYBEL_0:def 5
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;
end;
definition
let N be RelStr;
attr N is directed means
:: WAYBEL_0:def 6
[#]N is directed;
end;
registration
let L be 1-sorted;
cluster non empty reflexive transitive antisymmetric directed
for strict NetStr over L;
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
:: WAYBEL_0:def 7
the mapping of N;
let i be Element of N;
func N.i -> Element of L equals
:: WAYBEL_0:def 8
(the mapping of N).i;
end;
definition
let L be non empty RelStr;
let N be non empty NetStr over L;
attr N is monotone means
:: WAYBEL_0:def 9
netmap(N,L) is monotone;
attr N is antitone means
:: WAYBEL_0:def 10
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
:: WAYBEL_0:def 11
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
:: WAYBEL_0:def 12
for i being Element of N ex j being Element of N st i <= j & N.j in X;
end;
theorem :: WAYBEL_0:8
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);
theorem :: WAYBEL_0:9
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;
theorem :: WAYBEL_0:10
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;
scheme :: WAYBEL_0:sch 1
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];
definition
let L be non empty RelStr;
let N be non empty NetStr over L;
attr N is eventually-directed means
:: WAYBEL_0:def 13
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
:: WAYBEL_0:def 14
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 :: WAYBEL_0:11
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;
theorem :: WAYBEL_0:12
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;
registration
let L be non empty RelStr;
cluster monotone -> eventually-directed for prenet of L;
cluster antitone -> eventually-filtered for prenet of L;
end;
registration
let L be non empty reflexive RelStr;
cluster monotone antitone strict for prenet of L;
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
:: WAYBEL_0:def 15
for x being Element of L holds x in it iff
ex y being Element of L st y >= x & y in X;
func uparrow X -> Subset of L means
:: WAYBEL_0:def 16
for x being Element of L holds x in it iff
ex y being Element of L st y <= x & y in X;
end;
theorem :: WAYBEL_0:13
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;
theorem :: WAYBEL_0:14
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};
theorem :: WAYBEL_0:15
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};
registration
let L be non empty reflexive RelStr;
let X be non empty Subset of L;
cluster downarrow X -> non empty;
cluster uparrow X -> non empty;
end;
theorem :: WAYBEL_0:16
for L being reflexive RelStr, X being Subset of L holds
X c= downarrow X & X c= uparrow X;
definition
let L be non empty RelStr;
let x be Element of L;
func downarrow x -> Subset of L equals
:: WAYBEL_0:def 17 :: Definition 1.3 (iii)
downarrow {x};
func uparrow x -> Subset of L equals
:: WAYBEL_0:def 18 :: Definition 1.3 (iv)
uparrow {x};
end;
theorem :: WAYBEL_0:17
for L being non empty RelStr, x,y being Element of L
holds y in downarrow x iff y <= x;
theorem :: WAYBEL_0:18
for L being non empty RelStr, x,y being Element of L
holds y in uparrow x iff x <= y;
theorem :: WAYBEL_0:19
for L being non empty reflexive antisymmetric RelStr
for x,y being Element of L st downarrow x = downarrow y holds x = y;
theorem :: WAYBEL_0:20
for L being non empty reflexive antisymmetric RelStr
for x,y being Element of L st uparrow x = uparrow y holds x = y;
theorem :: WAYBEL_0:21
for L being non empty transitive RelStr for x,y being Element of L st x <= y
holds downarrow x c= downarrow y;
theorem :: WAYBEL_0:22
for L being non empty transitive RelStr for x,y being Element of L st x <= y
holds uparrow y c= uparrow x;
registration
let L be non empty reflexive RelStr;
let x be Element of L;
cluster downarrow x -> non empty directed;
cluster uparrow x -> non empty filtered;
end;
definition
let L be RelStr;
let X be Subset of L;
attr X is lower means
:: WAYBEL_0:def 19
:: 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
:: WAYBEL_0:def 20
:: 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;
end;
theorem :: WAYBEL_0:23
for L being RelStr, X being Subset of L holds X is lower iff downarrow X c= X
;
theorem :: WAYBEL_0:24
for L being RelStr, X being Subset of L holds X is upper iff uparrow X c= X;
theorem :: WAYBEL_0:25
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);
theorem :: WAYBEL_0:26
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;
theorem :: WAYBEL_0:27
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;
theorem :: WAYBEL_0:28
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;
theorem :: WAYBEL_0:29
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;
registration
let L be non empty transitive RelStr;
let X be Subset of L;
cluster downarrow X -> lower;
cluster uparrow X -> upper;
end;
registration
let L be non empty transitive RelStr;
let x be Element of L;
cluster downarrow x -> lower;
cluster uparrow x -> upper;
end;
registration
let L be non empty RelStr;
cluster [#]L -> lower upper;
end;
registration
let L be non empty RelStr;
cluster non empty lower upper for Subset of L;
end;
registration
let L be non empty reflexive transitive RelStr;
cluster non empty lower directed for Subset of L;
cluster non empty upper filtered for Subset of L;
end;
registration
let L be with_infima with_suprema Poset;
cluster non empty directed filtered lower upper for Subset of L;
end;
theorem :: WAYBEL_0:30
for L being non empty transitive reflexive RelStr, X be Subset of L holds
X is directed iff downarrow X is directed;
registration
let L be non empty transitive reflexive RelStr;
let X be directed Subset of L;
cluster downarrow X -> directed;
end;
theorem :: WAYBEL_0:31
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;
theorem :: WAYBEL_0:32
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;
theorem :: WAYBEL_0:33
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;
theorem :: WAYBEL_0:34
for L being non empty Poset, x being Element of L holds
ex_sup_of downarrow x, L & sup downarrow x = x;
theorem :: WAYBEL_0:35
for L being non empty transitive reflexive RelStr, X be Subset of L holds
X is filtered iff uparrow X is filtered;
registration
let L be non empty transitive reflexive RelStr;
let X be filtered Subset of L;
cluster uparrow X -> filtered;
end;
theorem :: WAYBEL_0:36
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;
theorem :: WAYBEL_0:37
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;
theorem :: WAYBEL_0:38
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;
theorem :: WAYBEL_0:39
for L being non empty Poset, x being Element of L holds
ex_inf_of uparrow x, L & inf uparrow x = x;
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 :: WAYBEL_0:40
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;
theorem :: WAYBEL_0:41
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;
theorem :: WAYBEL_0:42
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;
theorem :: WAYBEL_0:43
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;
theorem :: WAYBEL_0:44
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;
theorem :: WAYBEL_0:45
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;
theorem :: WAYBEL_0:46
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;
theorem :: WAYBEL_0:47
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;
definition
let L be non empty reflexive transitive RelStr;
let I be Ideal of L;
attr I is principal means
:: WAYBEL_0:def 21
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
:: WAYBEL_0:def 22
ex x being Element of L st x in F & x is_<=_than F;
end;
theorem :: WAYBEL_0:48
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;
theorem :: WAYBEL_0:49
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;
definition
let L be non empty reflexive transitive RelStr;
func Ids L -> set equals
:: WAYBEL_0:def 23 :: Definition 1.3 (xi)
the set of all X where X is Ideal of L;
func Filt L -> set equals
:: WAYBEL_0:def 24 :: Definition 1.3 (xi)
the set of all X where X is Filter of L;
end;
definition
let L be non empty reflexive transitive RelStr;
func Ids_0 L -> set equals
:: WAYBEL_0:def 25 :: Definition 1.3 (xii)
Ids L \/ {{}};
func Filt_0 L -> set equals
:: WAYBEL_0:def 26 :: Definition 1.3 (xiii)
Filt L \/ {{}};
end;
definition
let L be non empty RelStr;
let X be Subset of L;
func finsups X -> Subset of L equals
:: WAYBEL_0:def 27
{"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L};
func fininfs X -> Subset of L equals
:: WAYBEL_0:def 28
{"/\"(Y,L) where Y is finite Subset of X: ex_inf_of Y,L};
end;
registration
let L be non empty antisymmetric lower-bounded RelStr;
let X be Subset of L;
cluster finsups X -> non empty;
end;
registration
let L be non empty antisymmetric upper-bounded RelStr;
let X be Subset of L;
cluster fininfs X -> non empty;
end;
registration
let L be non empty reflexive antisymmetric RelStr;
let X be non empty Subset of L;
cluster finsups X -> non empty;
cluster fininfs X -> non empty;
end;
theorem :: WAYBEL_0:50
for L being non empty reflexive antisymmetric RelStr for X being Subset of L
holds X c= finsups X & X c= fininfs X;
theorem :: WAYBEL_0:51
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;
registration
let L be with_suprema Poset;
let X be Subset of L;
cluster finsups X -> directed;
end;
theorem :: WAYBEL_0:52
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;
theorem :: WAYBEL_0:53
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;
theorem :: WAYBEL_0:54
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;
theorem :: WAYBEL_0:55
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;
theorem :: WAYBEL_0:56
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;
registration
let L be with_infima Poset;
let X be Subset of L;
cluster fininfs X -> filtered;
end;
theorem :: WAYBEL_0:57
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;
theorem :: WAYBEL_0:58
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;
theorem :: WAYBEL_0:59
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;
theorem :: WAYBEL_0:60
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;
theorem :: WAYBEL_0:61
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;
theorem :: WAYBEL_0:62
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;
begin :: Chains
definition
let L be non empty RelStr;
attr L is connected means
:: WAYBEL_0:def 29
for x,y being Element of L holds x <= y or y <= x;
end;
registration
cluster trivial -> connected for non empty reflexive RelStr;
end;
registration
cluster connected for non empty Poset;
end;
definition
mode Chain is connected non empty Poset;
end;
registration
let L be Chain;
cluster L~ -> connected;
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 :: WAYBEL_0:63
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;
theorem :: WAYBEL_0:64
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;
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
:: WAYBEL_0:def 30
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
:: WAYBEL_0:def 31
ex_sup_of X,S implies ex_sup_of f.:X,T & sup (f.:X) = f.sup X;
end;
theorem :: WAYBEL_0:65
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);
definition
let L1,L2 be non empty RelStr;
let f be Function of L1,L2;
attr f is infs-preserving means
:: WAYBEL_0:def 32
for X being Subset of L1 holds f preserves_inf_of X;
attr f is sups-preserving means
:: WAYBEL_0:def 33
for X being Subset of L1 holds f preserves_sup_of X;
attr f is meet-preserving means
:: WAYBEL_0:def 34
for x,y being Element of L1 holds f preserves_inf_of {x,y};
attr f is join-preserving means
:: WAYBEL_0:def 35
for x,y being Element of L1 holds f preserves_sup_of {x,y};
attr f is filtered-infs-preserving means
:: WAYBEL_0:def 36
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
:: WAYBEL_0:def 37
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;
cluster sups-preserving ->
directed-sups-preserving join-preserving for Function of L1,L2;
end;
definition
let S,T be RelStr;
let f be Function of S,T;
attr f is isomorphic means
:: WAYBEL_0:def 38
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;
end;
theorem :: WAYBEL_0:66
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;
registration
let S,T be non empty RelStr;
cluster isomorphic -> one-to-one monotone for Function of S,T;
end;
theorem :: WAYBEL_0:67
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;
theorem :: WAYBEL_0:68
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;
theorem :: WAYBEL_0:69
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;
theorem :: WAYBEL_0:70
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;
theorem :: WAYBEL_0:71
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;
theorem :: WAYBEL_0:72
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;
theorem :: WAYBEL_0:73
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;
theorem :: WAYBEL_0:74
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;
begin :: Complete Semilattice
definition
let L be non empty reflexive RelStr;
attr L is up-complete means
:: WAYBEL_0:def 39
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;
end;
theorem :: WAYBEL_0:75
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;
definition
let L be non empty reflexive RelStr;
attr L is /\-complete means
:: WAYBEL_0:def 40
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 :: WAYBEL_0:76
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;
registration
cluster complete -> up-complete /\-complete for non empty reflexive RelStr;
cluster /\-complete -> lower-bounded for non empty reflexive RelStr;
cluster up-complete with_suprema lower-bounded -> complete for
non empty Poset;
:: 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;
end;
registration
cluster /\-complete -> with_suprema
for non empty reflexive antisymmetric upper-bounded RelStr;
end;
registration
cluster complete strict for LATTICE;
end;