:: WAYBEL12 semantic presentation begin Lm1: for L being non empty RelStr for f being Function of NAT, the carrier of L for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L proof let L be non empty RelStr ; ::_thesis: for f being Function of NAT, the carrier of L for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L let f be Function of NAT, the carrier of L; ::_thesis: for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L let n be Element of NAT ; ::_thesis: { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L set A = { (f . m) where m is Element of NAT : m <= n } ; A1: { (f . m) where m is Element of NAT : m <= n } c= { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (f . m) where m is Element of NAT : m <= n } or q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } ) assume q in { (f . m) where m is Element of NAT : m <= n } ; ::_thesis: q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } then consider m being Element of NAT such that A2: q = f . m and A3: m <= n ; A4: ( m = 0 or m in Seg m ) by FINSEQ_1:3; Seg m c= Seg n by A3, FINSEQ_1:5; then ( m in {0} or m in Seg n ) by A4, TARSKI:def_1; then m in {0} \/ (Seg n) by XBOOLE_0:def_3; hence q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } by A2; ::_thesis: verum end; deffunc H1( set ) -> set = f . \$1; A5: { (f . m) where m is Element of NAT : m <= n } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (f . m) where m is Element of NAT : m <= n } or q in the carrier of L ) assume q in { (f . m) where m is Element of NAT : m <= n } ; ::_thesis: q in the carrier of L then ex m being Element of NAT st ( q = f . m & m <= n ) ; hence q in the carrier of L ; ::_thesis: verum end; card { H1(m) where m is Element of NAT : m in {0} \/ (Seg n) } c= card ({0} \/ (Seg n)) from TREES_2:sch_2(); then A6: { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } is finite ; 0 <= n by NAT_1:2; then f . 0 in { (f . m) where m is Element of NAT : m <= n } ; hence { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L by A1, A6, A5; ::_thesis: verum end; definition let T be TopStruct ; let P be Subset of T; redefine attr P is closed means :: WAYBEL12:def 1 P ` is open ; compatibility ( P is closed iff P ` is open ) proof hereby ::_thesis: ( P ` is open implies P is closed ) assume P is closed ; ::_thesis: P ` is open then ([#] T) \ P is open by PRE_TOPC:def_3; hence P ` is open ; ::_thesis: verum end; assume P ` is open ; ::_thesis: P is closed hence ([#] T) \ P is open ; :: according to PRE_TOPC:def_3 ::_thesis: verum end; end; :: deftheorem defines closed WAYBEL12:def_1_:_ for T being TopStruct for P being Subset of T holds ( P is closed iff P ` is open ); definition let T be TopStruct ; let F be Subset-Family of T; attrF is dense means :Def2: :: WAYBEL12:def 2 for X being Subset of T st X in F holds X is dense ; end; :: deftheorem Def2 defines dense WAYBEL12:def_2_:_ for T being TopStruct for F being Subset-Family of T holds ( F is dense iff for X being Subset of T st X in F holds X is dense ); theorem Th1: :: WAYBEL12:1 for X, Y being set st card X c= card Y & Y is countable holds X is countable proof let X, Y be set ; ::_thesis: ( card X c= card Y & Y is countable implies X is countable ) assume A1: card X c= card Y ; ::_thesis: ( not Y is countable or X is countable ) assume card Y c= omega ; :: according to CARD_3:def_14 ::_thesis: X is countable hence card X c= omega by A1, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum end; theorem :: WAYBEL12:2 for A being denumerable set holds NAT ,A are_equipotent proof let A be denumerable set ; ::_thesis: NAT ,A are_equipotent not card A in omega ; then A1: omega c= card A by CARD_1:4; card A c= omega by CARD_3:def_14; then card NAT = card A by A1, CARD_1:47, XBOOLE_0:def_10; hence NAT ,A are_equipotent by CARD_1:5; ::_thesis: verum end; theorem :: WAYBEL12:3 for L being non empty transitive RelStr for A, B being Subset of L st A is_finer_than B holds downarrow A c= downarrow B proof let L be non empty transitive RelStr ; ::_thesis: for A, B being Subset of L st A is_finer_than B holds downarrow A c= downarrow B let A, B be Subset of L; ::_thesis: ( A is_finer_than B implies downarrow A c= downarrow B ) assume A1: for a being Element of L st a in A holds ex b being Element of L st ( b in B & b >= a ) ; :: according to YELLOW_4:def_1 ::_thesis: downarrow A c= downarrow B let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow A or q in downarrow B ) assume A2: q in downarrow A ; ::_thesis: q in downarrow B then reconsider q1 = q as Element of L ; consider a being Element of L such that A3: a >= q1 and A4: a in A by A2, WAYBEL_0:def_15; consider b being Element of L such that A5: b in B and A6: b >= a by A1, A4; b >= q1 by A3, A6, ORDERS_2:3; hence q in downarrow B by A5, WAYBEL_0:def_15; ::_thesis: verum end; theorem Th4: :: WAYBEL12:4 for L being non empty transitive RelStr for A, B being Subset of L st A is_coarser_than B holds uparrow A c= uparrow B proof let L be non empty transitive RelStr ; ::_thesis: for A, B being Subset of L st A is_coarser_than B holds uparrow A c= uparrow B let A, B be Subset of L; ::_thesis: ( A is_coarser_than B implies uparrow A c= uparrow B ) assume A1: for a being Element of L st a in A holds ex b being Element of L st ( b in B & b <= a ) ; :: according to YELLOW_4:def_2 ::_thesis: uparrow A c= uparrow B let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow A or q in uparrow B ) assume A2: q in uparrow A ; ::_thesis: q in uparrow B then reconsider q1 = q as Element of L ; consider a being Element of L such that A3: a <= q1 and A4: a in A by A2, WAYBEL_0:def_16; consider b being Element of L such that A5: b in B and A6: b <= a by A1, A4; b <= q1 by A3, A6, ORDERS_2:3; hence q in uparrow B by A5, WAYBEL_0:def_16; ::_thesis: verum end; theorem :: WAYBEL12:5 for L being non empty Poset for D being non empty finite filtered Subset of L st ex_inf_of D,L holds inf D in D proof let L be non empty Poset; ::_thesis: for D being non empty finite filtered Subset of L st ex_inf_of D,L holds inf D in D let D be non empty finite filtered Subset of L; ::_thesis: ( ex_inf_of D,L implies inf D in D ) assume A1: ex_inf_of D,L ; ::_thesis: inf D in D D c= D ; then consider d being Element of L such that A2: d in D and A3: d is_<=_than D by WAYBEL_0:2; A4: inf D >= d by A1, A3, YELLOW_0:31; inf D is_<=_than D by A1, YELLOW_0:31; then inf D <= d by A2, LATTICE3:def_8; hence inf D in D by A2, A4, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL12:6 for L being non empty antisymmetric lower-bounded RelStr for X being non empty lower Subset of L holds Bottom L in X proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for X being non empty lower Subset of L holds Bottom L in X let X be non empty lower Subset of L; ::_thesis: Bottom L in X consider y being set such that A1: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A1; Bottom L <= y by YELLOW_0:44; hence Bottom L in X by WAYBEL_0:def_19; ::_thesis: verum end; theorem :: WAYBEL12:7 for L being non empty antisymmetric lower-bounded RelStr for X being non empty Subset of L holds Bottom L in downarrow X proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for X being non empty Subset of L holds Bottom L in downarrow X let X be non empty Subset of L; ::_thesis: Bottom L in downarrow X consider y being set such that A1: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A1; ( downarrow X = { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } & Bottom L <= y ) by WAYBEL_0:14, YELLOW_0:44; hence Bottom L in downarrow X ; ::_thesis: verum end; theorem Th8: :: WAYBEL12:8 for L being non empty antisymmetric upper-bounded RelStr for X being non empty upper Subset of L holds Top L in X proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for X being non empty upper Subset of L holds Top L in X let X be non empty upper Subset of L; ::_thesis: Top L in X consider y being set such that A1: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A1; Top L >= y by YELLOW_0:45; hence Top L in X by WAYBEL_0:def_20; ::_thesis: verum end; theorem Th9: :: WAYBEL12:9 for L being non empty antisymmetric upper-bounded RelStr for X being non empty Subset of L holds Top L in uparrow X proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for X being non empty Subset of L holds Top L in uparrow X let X be non empty Subset of L; ::_thesis: Top L in uparrow X consider y being set such that A1: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A1; ( uparrow X = { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } & Top L >= y ) by WAYBEL_0:15, YELLOW_0:45; hence Top L in uparrow X ; ::_thesis: verum end; theorem Th10: :: WAYBEL12:10 for L being antisymmetric lower-bounded with_infima RelStr for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)} proof let L be antisymmetric lower-bounded with_infima RelStr ; ::_thesis: for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)} let X be Subset of L; ::_thesis: X "/\" {(Bottom L)} c= {(Bottom L)} A1: {(Bottom L)} "/\" X = { ((Bottom L) "/\" y) where y is Element of L : y in X } by YELLOW_4:42; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "/\" {(Bottom L)} or q in {(Bottom L)} ) assume q in X "/\" {(Bottom L)} ; ::_thesis: q in {(Bottom L)} then consider y being Element of L such that A2: q = (Bottom L) "/\" y and y in X by A1; y "/\" (Bottom L) = Bottom L by WAYBEL_1:3; hence q in {(Bottom L)} by A2, TARSKI:def_1; ::_thesis: verum end; theorem :: WAYBEL12:11 for L being antisymmetric lower-bounded with_infima RelStr for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)} proof let L be antisymmetric lower-bounded with_infima RelStr ; ::_thesis: for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)} let X be non empty Subset of L; ::_thesis: X "/\" {(Bottom L)} = {(Bottom L)} thus X "/\" {(Bottom L)} c= {(Bottom L)} by Th10; :: according to XBOOLE_0:def_10 ::_thesis: {(Bottom L)} c= X "/\" {(Bottom L)} let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Bottom L)} or q in X "/\" {(Bottom L)} ) assume q in {(Bottom L)} ; ::_thesis: q in X "/\" {(Bottom L)} then A1: ( X "/\" {(Bottom L)} = { ((Bottom L) "/\" y) where y is Element of L : y in X } & q = Bottom L ) by TARSKI:def_1, YELLOW_4:42; consider y being set such that A2: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A2; (Bottom L) "/\" y = Bottom L by WAYBEL_1:3; hence q in X "/\" {(Bottom L)} by A1; ::_thesis: verum end; theorem Th12: :: WAYBEL12:12 for L being antisymmetric upper-bounded with_suprema RelStr for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)} proof let L be antisymmetric upper-bounded with_suprema RelStr ; ::_thesis: for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)} let X be Subset of L; ::_thesis: X "\/" {(Top L)} c= {(Top L)} A1: {(Top L)} "\/" X = { ((Top L) "\/" y) where y is Element of L : y in X } by YELLOW_4:15; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "\/" {(Top L)} or q in {(Top L)} ) assume q in X "\/" {(Top L)} ; ::_thesis: q in {(Top L)} then consider y being Element of L such that A2: q = (Top L) "\/" y and y in X by A1; y "\/" (Top L) = Top L by WAYBEL_1:4; hence q in {(Top L)} by A2, TARSKI:def_1; ::_thesis: verum end; theorem :: WAYBEL12:13 for L being antisymmetric upper-bounded with_suprema RelStr for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)} proof let L be antisymmetric upper-bounded with_suprema RelStr ; ::_thesis: for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)} let X be non empty Subset of L; ::_thesis: X "\/" {(Top L)} = {(Top L)} thus X "\/" {(Top L)} c= {(Top L)} by Th12; :: according to XBOOLE_0:def_10 ::_thesis: {(Top L)} c= X "\/" {(Top L)} let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Top L)} or q in X "\/" {(Top L)} ) assume q in {(Top L)} ; ::_thesis: q in X "\/" {(Top L)} then A1: ( X "\/" {(Top L)} = { ((Top L) "\/" y) where y is Element of L : y in X } & q = Top L ) by TARSKI:def_1, YELLOW_4:15; consider y being set such that A2: y in X by XBOOLE_0:def_1; reconsider y = y as Element of X by A2; (Top L) "\/" y = Top L by WAYBEL_1:4; hence q in X "\/" {(Top L)} by A1; ::_thesis: verum end; theorem Th14: :: WAYBEL12:14 for L being upper-bounded Semilattice for X being Subset of L holds {(Top L)} "/\" X = X proof let L be upper-bounded Semilattice; ::_thesis: for X being Subset of L holds {(Top L)} "/\" X = X let X be Subset of L; ::_thesis: {(Top L)} "/\" X = X A1: {(Top L)} "/\" X = { ((Top L) "/\" y) where y is Element of L : y in X } by YELLOW_4:42; thus {(Top L)} "/\" X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= {(Top L)} "/\" X proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Top L)} "/\" X or q in X ) assume q in {(Top L)} "/\" X ; ::_thesis: q in X then ex y being Element of L st ( q = (Top L) "/\" y & y in X ) by A1; hence q in X by WAYBEL_1:4; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in {(Top L)} "/\" X ) assume A2: q in X ; ::_thesis: q in {(Top L)} "/\" X then reconsider X1 = X as non empty Subset of L ; reconsider y = q as Element of X1 by A2; q = (Top L) "/\" y by WAYBEL_1:4; hence q in {(Top L)} "/\" X by A1; ::_thesis: verum end; theorem :: WAYBEL12:15 for L being lower-bounded with_suprema Poset for X being Subset of L holds {(Bottom L)} "\/" X = X proof let L be lower-bounded with_suprema Poset; ::_thesis: for X being Subset of L holds {(Bottom L)} "\/" X = X let X be Subset of L; ::_thesis: {(Bottom L)} "\/" X = X A1: {(Bottom L)} "\/" X = { ((Bottom L) "\/" y) where y is Element of L : y in X } by YELLOW_4:15; thus {(Bottom L)} "\/" X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= {(Bottom L)} "\/" X proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Bottom L)} "\/" X or q in X ) assume q in {(Bottom L)} "\/" X ; ::_thesis: q in X then ex y being Element of L st ( q = (Bottom L) "\/" y & y in X ) by A1; hence q in X by WAYBEL_1:3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in {(Bottom L)} "\/" X ) assume A2: q in X ; ::_thesis: q in {(Bottom L)} "\/" X then reconsider X1 = X as non empty Subset of L ; reconsider y = q as Element of X1 by A2; q = (Bottom L) "\/" y by WAYBEL_1:3; hence q in {(Bottom L)} "\/" X by A1; ::_thesis: verum end; theorem Th16: :: WAYBEL12:16 for L being non empty reflexive RelStr for A, B being Subset of L st A c= B holds ( A is_finer_than B & A is_coarser_than B ) proof let L be non empty reflexive RelStr ; ::_thesis: for A, B being Subset of L st A c= B holds ( A is_finer_than B & A is_coarser_than B ) let A, B be Subset of L; ::_thesis: ( A c= B implies ( A is_finer_than B & A is_coarser_than B ) ) assume A1: A c= B ; ::_thesis: ( A is_finer_than B & A is_coarser_than B ) thus A is_finer_than B ::_thesis: A is_coarser_than B proof let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st ( b1 in B & a <= b1 ) ) assume A2: a in A ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in B & a <= b1 ) take b = a; ::_thesis: ( b in B & a <= b ) thus ( b in B & a <= b ) by A1, A2; ::_thesis: verum end; let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st ( b1 in B & b1 <= a ) ) assume A3: a in A ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in B & b1 <= a ) take b = a; ::_thesis: ( b in B & b <= a ) thus ( b in B & b <= a ) by A1, A3; ::_thesis: verum end; theorem Th17: :: WAYBEL12:17 for L being transitive antisymmetric with_infima RelStr for V being Subset of L for x, y being Element of L st x <= y holds {y} "/\" V is_coarser_than {x} "/\" V proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being Subset of L for x, y being Element of L st x <= y holds {y} "/\" V is_coarser_than {x} "/\" V let V be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds {y} "/\" V is_coarser_than {x} "/\" V let x, y be Element of L; ::_thesis: ( x <= y implies {y} "/\" V is_coarser_than {x} "/\" V ) assume A1: x <= y ; ::_thesis: {y} "/\" V is_coarser_than {x} "/\" V A2: {y} "/\" V = { (y "/\" s) where s is Element of L : s in V } by YELLOW_4:42; let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not b in {y} "/\" V or ex b1 being Element of the carrier of L st ( b1 in {x} "/\" V & b1 <= b ) ) assume b in {y} "/\" V ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in {x} "/\" V & b1 <= b ) then consider s being Element of L such that A3: b = y "/\" s and A4: s in V by A2; take a = x "/\" s; ::_thesis: ( a in {x} "/\" V & a <= b ) {x} "/\" V = { (x "/\" t) where t is Element of L : t in V } by YELLOW_4:42; hence a in {x} "/\" V by A4; ::_thesis: a <= b thus a <= b by A1, A3, WAYBEL_1:1; ::_thesis: verum end; theorem :: WAYBEL12:18 for L being transitive antisymmetric with_suprema RelStr for V being Subset of L for x, y being Element of L st x <= y holds {x} "\/" V is_finer_than {y} "\/" V proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for V being Subset of L for x, y being Element of L st x <= y holds {x} "\/" V is_finer_than {y} "\/" V let V be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds {x} "\/" V is_finer_than {y} "\/" V let x, y be Element of L; ::_thesis: ( x <= y implies {x} "\/" V is_finer_than {y} "\/" V ) assume A1: x <= y ; ::_thesis: {x} "\/" V is_finer_than {y} "\/" V A2: {x} "\/" V = { (x "\/" s) where s is Element of L : s in V } by YELLOW_4:15; let b be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( not b in {x} "\/" V or ex b1 being Element of the carrier of L st ( b1 in {y} "\/" V & b <= b1 ) ) assume b in {x} "\/" V ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in {y} "\/" V & b <= b1 ) then consider s being Element of L such that A3: b = x "\/" s and A4: s in V by A2; take a = y "\/" s; ::_thesis: ( a in {y} "\/" V & b <= a ) {y} "\/" V = { (y "\/" t) where t is Element of L : t in V } by YELLOW_4:15; hence a in {y} "\/" V by A4; ::_thesis: b <= a thus b <= a by A1, A3, WAYBEL_1:2; ::_thesis: verum end; theorem Th19: :: WAYBEL12:19 for L being non empty RelStr for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds S c= V proof let L be non empty RelStr ; ::_thesis: for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds S c= V let V, S, T be Subset of L; ::_thesis: ( S is_coarser_than T & V is upper & T c= V implies S c= V ) assume that A1: S is_coarser_than T and A2: ( V is upper & T c= V ) ; ::_thesis: S c= V let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in S or q in V ) assume A3: q in S ; ::_thesis: q in V then reconsider S1 = S as non empty Subset of L ; reconsider b = q as Element of S1 by A3; ex a being Element of L st ( a in T & a <= b ) by A1, YELLOW_4:def_2; hence q in V by A2, WAYBEL_0:def_20; ::_thesis: verum end; theorem :: WAYBEL12:20 for L being non empty RelStr for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds S c= V proof let L be non empty RelStr ; ::_thesis: for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds S c= V let V, S, T be Subset of L; ::_thesis: ( S is_finer_than T & V is lower & T c= V implies S c= V ) assume that A1: S is_finer_than T and A2: ( V is lower & T c= V ) ; ::_thesis: S c= V let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in S or q in V ) assume A3: q in S ; ::_thesis: q in V then reconsider S1 = S as non empty Subset of L ; reconsider a = q as Element of S1 by A3; ex b being Element of L st ( b in T & a <= b ) by A1, YELLOW_4:def_1; hence q in V by A2, WAYBEL_0:def_19; ::_thesis: verum end; theorem Th21: :: WAYBEL12:21 for L being Semilattice for F being filtered upper Subset of L holds F "/\" F = F proof let L be Semilattice; ::_thesis: for F being filtered upper Subset of L holds F "/\" F = F let F be filtered upper Subset of L; ::_thesis: F "/\" F = F thus F "/\" F c= F :: according to XBOOLE_0:def_10 ::_thesis: F c= F "/\" F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F "/\" F or x in F ) assume x in F "/\" F ; ::_thesis: x in F then consider y, z being Element of L such that A1: x = y "/\" z and A2: ( y in F & z in F ) ; consider t being Element of L such that A3: t in F and A4: ( t <= y & t <= z ) by A2, WAYBEL_0:def_2; y "/\" z >= t by A4, YELLOW_0:23; hence x in F by A1, A3, WAYBEL_0:def_20; ::_thesis: verum end; thus F c= F "/\" F by YELLOW_4:40; ::_thesis: verum end; theorem :: WAYBEL12:22 for L being sup-Semilattice for I being directed lower Subset of L holds I "\/" I = I proof let L be sup-Semilattice; ::_thesis: for I being directed lower Subset of L holds I "\/" I = I let I be directed lower Subset of L; ::_thesis: I "\/" I = I thus I "\/" I c= I :: according to XBOOLE_0:def_10 ::_thesis: I c= I "\/" I proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I "\/" I or x in I ) assume x in I "\/" I ; ::_thesis: x in I then consider y, z being Element of L such that A1: x = y "\/" z and A2: ( y in I & z in I ) ; consider t being Element of L such that A3: t in I and A4: ( t >= y & t >= z ) by A2, WAYBEL_0:def_1; y "\/" z <= t by A4, YELLOW_0:22; hence x in I by A1, A3, WAYBEL_0:def_19; ::_thesis: verum end; thus I c= I "\/" I by YELLOW_4:13; ::_thesis: verum end; Lm2: for L being non empty RelStr for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L proof let L be non empty RelStr ; ::_thesis: for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L let V be Subset of L; ::_thesis: { x where x is Element of L : V "/\" {x} c= V } is Subset of L set G = { x where x is Element of L : V "/\" {x} c= V } ; { x where x is Element of L : V "/\" {x} c= V } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { x where x is Element of L : V "/\" {x} c= V } or q in the carrier of L ) assume q in { x where x is Element of L : V "/\" {x} c= V } ; ::_thesis: q in the carrier of L then ex x being Element of L st ( q = x & V "/\" {x} c= V ) ; hence q in the carrier of L ; ::_thesis: verum end; hence { x where x is Element of L : V "/\" {x} c= V } is Subset of L ; ::_thesis: verum end; theorem Th23: :: WAYBEL12:23 for L being upper-bounded Semilattice for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty proof let L be upper-bounded Semilattice; ::_thesis: for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty let V be Subset of L; ::_thesis: not { x where x is Element of L : V "/\" {x} c= V } is empty set G = { x where x is Element of L : V "/\" {x} c= V } ; V "/\" {(Top L)} = V by Th14; then Top L in { x where x is Element of L : V "/\" {x} c= V } ; hence not { x where x is Element of L : V "/\" {x} c= V } is empty ; ::_thesis: verum end; theorem Th24: :: WAYBEL12:24 for L being transitive antisymmetric with_infima RelStr for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L let V be Subset of L; ::_thesis: { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L reconsider G1 = { x where x is Element of L : V "/\" {x} c= V } as Subset of L by Lm2; G1 is filtered proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in G1 or not y in G1 or ex b1 being Element of the carrier of L st ( b1 in G1 & b1 <= x & b1 <= y ) ) assume x in G1 ; ::_thesis: ( not y in G1 or ex b1 being Element of the carrier of L st ( b1 in G1 & b1 <= x & b1 <= y ) ) then consider x1 being Element of L such that A1: x = x1 and A2: V "/\" {x1} c= V ; assume y in G1 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in G1 & b1 <= x & b1 <= y ) then consider y1 being Element of L such that A3: y = y1 and A4: V "/\" {y1} c= V ; take z = x1 "/\" y1; ::_thesis: ( z in G1 & z <= x & z <= y ) V "/\" {z} c= V proof A5: {z} "/\" V = { (z "/\" v) where v is Element of L : v in V } by YELLOW_4:42; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in V "/\" {z} or q in V ) assume q in V "/\" {z} ; ::_thesis: q in V then consider v being Element of L such that A6: q = z "/\" v and A7: v in V by A5; A8: ( {x1} "/\" V = { (x1 "/\" s) where s is Element of L : s in V } & q = x1 "/\" (y1 "/\" v) ) by A6, LATTICE3:16, YELLOW_4:42; {y1} "/\" V = { (y1 "/\" t) where t is Element of L : t in V } by YELLOW_4:42; then y1 "/\" v in V "/\" {y1} by A7; then q in V "/\" {x1} by A4, A8; hence q in V by A2; ::_thesis: verum end; hence z in G1 ; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by A1, A3, YELLOW_0:23; ::_thesis: verum end; hence { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L ; ::_thesis: verum end; theorem Th25: :: WAYBEL12:25 for L being transitive antisymmetric with_infima RelStr for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L let V be upper Subset of L; ::_thesis: { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L reconsider G1 = { x where x is Element of L : V "/\" {x} c= V } as Subset of L by Lm2; G1 is upper proof let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in G1 or not x <= y or y in G1 ) assume x in G1 ; ::_thesis: ( not x <= y or y in G1 ) then A1: ex x1 being Element of L st ( x1 = x & V "/\" {x1} c= V ) ; assume x <= y ; ::_thesis: y in G1 then V "/\" {y} c= V by A1, Th17, Th19; hence y in G1 ; ::_thesis: verum end; hence { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L ; ::_thesis: verum end; theorem Th26: :: WAYBEL12:26 for L being with_infima Poset for X being Subset of L st X is Open & X is lower holds X is filtered proof let L be with_infima Poset; ::_thesis: for X being Subset of L st X is Open & X is lower holds X is filtered let X be Subset of L; ::_thesis: ( X is Open & X is lower implies X is filtered ) assume A1: ( X is Open & X is lower ) ; ::_thesis: X is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of L st ( b1 in X & b1 <= x & b1 <= y ) ) assume that A2: x in X and y in X ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in X & b1 <= x & b1 <= y ) A3: x "/\" y <= x by YELLOW_0:23; then x "/\" y in X by A1, A2, WAYBEL_0:def_19; then consider z being Element of L such that A4: z in X and A5: z << x "/\" y by A1, WAYBEL_6:def_1; take z ; ::_thesis: ( z in X & z <= x & z <= y ) ( x "/\" y <= y & z <= x "/\" y ) by A5, WAYBEL_3:1, YELLOW_0:23; hence ( z in X & z <= x & z <= y ) by A3, A4, ORDERS_2:3; ::_thesis: verum end; registration let L be with_infima Poset; cluster lower Open -> filtered for Element of bool the carrier of L; coherence for b1 being Subset of L st b1 is Open & b1 is lower holds b1 is filtered by Th26; end; registration let L be non empty reflexive antisymmetric continuous RelStr ; cluster lower -> Open for Element of bool the carrier of L; coherence for b1 being Subset of L st b1 is lower holds b1 is Open proof let A be Subset of L; ::_thesis: ( A is lower implies A is Open ) assume A1: A is lower ; ::_thesis: A is Open let x be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in A or ex b1 being Element of the carrier of L st ( b1 in A & b1 is_way_below x ) ) assume A2: x in A ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in A & b1 is_way_below x ) consider y being set such that A3: y in waybelow x by XBOOLE_0:def_1; reconsider y = y as Element of L by A3; take y ; ::_thesis: ( y in A & y is_way_below x ) y << x by A3, WAYBEL_3:7; then y <= x by WAYBEL_3:1; hence ( y in A & y is_way_below x ) by A1, A2, A3, WAYBEL_0:def_19, WAYBEL_3:7; ::_thesis: verum end; end; registration let L be continuous Semilattice; let x be Element of L; cluster(downarrow x) ` -> Open ; coherence (downarrow x) ` is Open proof let a be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not a in (downarrow x) ` or ex b1 being Element of the carrier of L st ( b1 in (downarrow x) ` & b1 is_way_below a ) ) set A = (downarrow x) ` ; assume a in (downarrow x) ` ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in (downarrow x) ` & b1 is_way_below a ) then not a in downarrow x by XBOOLE_0:def_5; then A1: not a <= x by WAYBEL_0:17; for x being Element of L holds ( not waybelow x is empty & waybelow x is directed ) ; then consider y being Element of L such that A2: y << a and A3: not y <= x by A1, WAYBEL_3:24; take y ; ::_thesis: ( y in (downarrow x) ` & y is_way_below a ) not y in downarrow x by A3, WAYBEL_0:17; hence y in (downarrow x) ` by XBOOLE_0:def_5; ::_thesis: y is_way_below a thus y is_way_below a by A2; ::_thesis: verum end; end; theorem Th27: :: WAYBEL12:27 for L being Semilattice for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) holds for Y being non empty finite Subset of C holds "/\" (Y,L) in Y proof let L be Semilattice; ::_thesis: for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) holds for Y being non empty finite Subset of C holds "/\" (Y,L) in Y let C be non empty Subset of L; ::_thesis: ( ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) implies for Y being non empty finite Subset of C holds "/\" (Y,L) in Y ) assume A1: for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ; ::_thesis: for Y being non empty finite Subset of C holds "/\" (Y,L) in Y defpred S1[ set ] means ( "/\" (\$1,L) in \$1 & ex_inf_of \$1,L ); A2: for B1, B2 being non empty Element of Fin C st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin C; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume A3: ( S1[B1] & S1[B2] ) ; ::_thesis: S1[B1 \/ B2] ( B1 c= C & B2 c= C ) by FINSUB_1:def_5; then ( "/\" (B1,L) <= "/\" (B2,L) or "/\" (B2,L) <= "/\" (B1,L) ) by A1, A3; then A4: ( ("/\" (B1,L)) "/\" ("/\" (B2,L)) = "/\" (B1,L) or ("/\" (B1,L)) "/\" ("/\" (B2,L)) = "/\" (B2,L) ) by YELLOW_0:25; "/\" ((B1 \/ B2),L) = ("/\" (B1,L)) "/\" ("/\" (B2,L)) by A3, YELLOW_2:4; hence S1[B1 \/ B2] by A3, A4, XBOOLE_0:def_3, YELLOW_2:4; ::_thesis: verum end; let Y be non empty finite Subset of C; ::_thesis: "/\" (Y,L) in Y A5: Y in Fin C by FINSUB_1:def_5; A6: for x being Element of C holds S1[{x}] proof let x be Element of C; ::_thesis: S1[{x}] "/\" ({x},L) = x by YELLOW_0:39; hence S1[{x}] by TARSKI:def_1, YELLOW_0:38; ::_thesis: verum end; for B being non empty Element of Fin C holds S1[B] from SETWISEO:sch_3(A6, A2); hence "/\" (Y,L) in Y by A5; ::_thesis: verum end; theorem :: WAYBEL12:28 for L being sup-Semilattice for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) holds for Y being non empty finite Subset of C holds "\/" (Y,L) in Y proof let L be sup-Semilattice; ::_thesis: for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) holds for Y being non empty finite Subset of C holds "\/" (Y,L) in Y let C be non empty Subset of L; ::_thesis: ( ( for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ) implies for Y being non empty finite Subset of C holds "\/" (Y,L) in Y ) assume A1: for x, y being Element of L st x in C & y in C & not x <= y holds y <= x ; ::_thesis: for Y being non empty finite Subset of C holds "\/" (Y,L) in Y defpred S1[ set ] means ( "\/" (\$1,L) in \$1 & ex_sup_of \$1,L ); A2: for B1, B2 being non empty Element of Fin C st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin C; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume A3: ( S1[B1] & S1[B2] ) ; ::_thesis: S1[B1 \/ B2] ( B1 c= C & B2 c= C ) by FINSUB_1:def_5; then ( "\/" (B1,L) <= "\/" (B2,L) or "\/" (B2,L) <= "\/" (B1,L) ) by A1, A3; then A4: ( ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B1,L) or ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B2,L) ) by YELLOW_0:24; "\/" ((B1 \/ B2),L) = ("\/" (B1,L)) "\/" ("\/" (B2,L)) by A3, YELLOW_2:3; hence S1[B1 \/ B2] by A3, A4, XBOOLE_0:def_3, YELLOW_2:3; ::_thesis: verum end; let Y be non empty finite Subset of C; ::_thesis: "\/" (Y,L) in Y A5: Y in Fin C by FINSUB_1:def_5; A6: for x being Element of C holds S1[{x}] proof let x be Element of C; ::_thesis: S1[{x}] "\/" ({x},L) = x by YELLOW_0:39; hence S1[{x}] by TARSKI:def_1, YELLOW_0:38; ::_thesis: verum end; for B being non empty Element of Fin C holds S1[B] from SETWISEO:sch_3(A6, A2); hence "\/" (Y,L) in Y by A5; ::_thesis: verum end; Lm3: for L being Semilattice for F being Filter of L holds F = uparrow (fininfs F) proof let L be Semilattice; ::_thesis: for F being Filter of L holds F = uparrow (fininfs F) let F be Filter of L; ::_thesis: F = uparrow (fininfs F) thus F c= uparrow (fininfs F) by WAYBEL_0:62; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (fininfs F) c= F thus uparrow (fininfs F) c= F by WAYBEL_0:62; ::_thesis: verum end; definition let L be Semilattice; let F be Filter of L; mode GeneratorSet of F -> Subset of L means :Def3: :: WAYBEL12:def 3 F = uparrow (fininfs it); existence ex b1 being Subset of L st F = uparrow (fininfs b1) proof take F ; ::_thesis: F = uparrow (fininfs F) thus F = uparrow (fininfs F) by Lm3; ::_thesis: verum end; end; :: deftheorem Def3 defines GeneratorSet WAYBEL12:def_3_:_ for L being Semilattice for F being Filter of L for b3 being Subset of L holds ( b3 is GeneratorSet of F iff F = uparrow (fininfs b3) ); registration let L be Semilattice; let F be Filter of L; cluster non empty for GeneratorSet of F; existence not for b1 being GeneratorSet of F holds b1 is empty proof F = uparrow (fininfs F) by Lm3; then reconsider F1 = F as GeneratorSet of F by Def3; take F1 ; ::_thesis: not F1 is empty thus not F1 is empty ; ::_thesis: verum end; end; Lm4: for L being Semilattice for F being Filter of L for G being GeneratorSet of F holds G c= F proof let L be Semilattice; ::_thesis: for F being Filter of L for G being GeneratorSet of F holds G c= F let F be Filter of L; ::_thesis: for G being GeneratorSet of F holds G c= F let G be GeneratorSet of F; ::_thesis: G c= F F = uparrow (fininfs G) by Def3; hence G c= F by WAYBEL_0:62; ::_thesis: verum end; theorem Th29: :: WAYBEL12:29 for L being Semilattice for A being Subset of L for B being non empty Subset of L st A is_coarser_than B holds fininfs A is_coarser_than fininfs B proof let L be Semilattice; ::_thesis: for A being Subset of L for B being non empty Subset of L st A is_coarser_than B holds fininfs A is_coarser_than fininfs B let A be Subset of L; ::_thesis: for B being non empty Subset of L st A is_coarser_than B holds fininfs A is_coarser_than fininfs B let B be non empty Subset of L; ::_thesis: ( A is_coarser_than B implies fininfs A is_coarser_than fininfs B ) assume A1: for a being Element of L st a in A holds ex b being Element of L st ( b in B & b <= a ) ; :: according to YELLOW_4:def_2 ::_thesis: fininfs A is_coarser_than fininfs B defpred S1[ set , set ] means ex x, y being Element of L st ( x = \$1 & y = \$2 & y <= x ); let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in fininfs A or ex b1 being Element of the carrier of L st ( b1 in fininfs B & b1 <= a ) ) assume a in fininfs A ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in fininfs B & b1 <= a ) then consider Y being finite Subset of A such that A2: a = "/\" (Y,L) and A3: ex_inf_of Y,L ; A4: for e being set st e in Y holds ex u being set st ( u in B & S1[e,u] ) proof let e be set ; ::_thesis: ( e in Y implies ex u being set st ( u in B & S1[e,u] ) ) assume A5: e in Y ; ::_thesis: ex u being set st ( u in B & S1[e,u] ) Y c= the carrier of L by XBOOLE_1:1; then reconsider e = e as Element of L by A5; ex b being Element of L st ( b in B & b <= e ) by A1, A5; hence ex u being set st ( u in B & S1[e,u] ) ; ::_thesis: verum end; consider f being Function of Y,B such that A6: for e being set st e in Y holds S1[e,f . e] from FUNCT_2:sch_1(A4); A7: f .: Y c= the carrier of L proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: Y or y in the carrier of L ) assume y in f .: Y ; ::_thesis: y in the carrier of L then consider x being set such that A8: x in dom f and x in Y and A9: y = f . x by FUNCT_1:def_6; f . x in B by A8, FUNCT_2:5; hence y in the carrier of L by A9; ::_thesis: verum end; A10: now__::_thesis:_(_(_Y_=_{}_&_ex_inf_of_f_.:_Y,L_)_or_(_Y_<>_{}_&_ex_inf_of_f_.:_Y,L_)_) percases ( Y = {} or Y <> {} ) ; case Y = {} ; ::_thesis: ex_inf_of f .: Y,L hence ex_inf_of f .: Y,L by A3; ::_thesis: verum end; case Y <> {} ; ::_thesis: ex_inf_of f .: Y,L then consider e being set such that A11: e in Y by XBOOLE_0:def_1; dom f = Y by FUNCT_2:def_1; then f . e in f .: Y by A11, FUNCT_1:def_6; hence ex_inf_of f .: Y,L by A7, YELLOW_0:55; ::_thesis: verum end; end; end; "/\" ((f .: Y),L) is_<=_than Y proof let e be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not e in Y or "/\" ((f .: Y),L) <= e ) assume A12: e in Y ; ::_thesis: "/\" ((f .: Y),L) <= e then consider x, y being Element of L such that A13: x = e and A14: y = f . e and A15: y <= x by A6; dom f = Y by FUNCT_2:def_1; then f . e in f .: Y by A12, FUNCT_1:def_6; then "/\" ((f .: Y),L) <= y by A10, A14, YELLOW_4:2; hence "/\" ((f .: Y),L) <= e by A13, A15, ORDERS_2:3; ::_thesis: verum end; then A16: "/\" ((f .: Y),L) <= "/\" (Y,L) by A3, YELLOW_0:31; "/\" ((f .: Y),L) in fininfs B by A10; hence ex b being Element of L st ( b in fininfs B & b <= a ) by A2, A16; ::_thesis: verum end; theorem Th30: :: WAYBEL12:30 for L being Semilattice for F being Filter of L for G being GeneratorSet of F for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds A is GeneratorSet of F proof let L be Semilattice; ::_thesis: for F being Filter of L for G being GeneratorSet of F for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds A is GeneratorSet of F let F be Filter of L; ::_thesis: for G being GeneratorSet of F for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds A is GeneratorSet of F let G be GeneratorSet of F; ::_thesis: for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds A is GeneratorSet of F let A be non empty Subset of L; ::_thesis: ( G is_coarser_than A & A is_coarser_than F implies A is GeneratorSet of F ) assume A1: G is_coarser_than A ; ::_thesis: ( not A is_coarser_than F or A is GeneratorSet of F ) assume A2: A is_coarser_than F ; ::_thesis: A is GeneratorSet of F F = uparrow (fininfs G) by Def3; hence F c= uparrow (fininfs A) by A1, Th4, Th29; :: according to XBOOLE_0:def_10,WAYBEL12:def_3 ::_thesis: uparrow (fininfs A) c= F A c= F by A2, YELLOW_4:8; hence uparrow (fininfs A) c= F by WAYBEL_0:62; ::_thesis: verum end; theorem Th31: :: WAYBEL12:31 for L being Semilattice for A being Subset of L for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds A is_coarser_than rng g proof let L be Semilattice; ::_thesis: for A being Subset of L for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds A is_coarser_than rng g let A be Subset of L; ::_thesis: for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds A is_coarser_than rng g let f, g be Function of NAT, the carrier of L; ::_thesis: ( rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies A is_coarser_than rng g ) assume that A1: rng f = A and A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; ::_thesis: A is_coarser_than rng g let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st ( b1 in rng g & b1 <= a ) ) assume a in A ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in rng g & b1 <= a ) then consider n being set such that A3: n in dom f and A4: f . n = a by A1, FUNCT_1:def_3; reconsider n = n as Element of NAT by A3; reconsider T = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1; take b = "/\" (T,L); ::_thesis: ( b in rng g & b <= a ) ( dom g = NAT & g . n = b ) by A2, FUNCT_2:def_1; hence b in rng g by FUNCT_1:def_3; ::_thesis: b <= a f . n in T ; then A5: {(f . n)} c= T by ZFMISC_1:31; ( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55; then b <= "/\" ({(f . n)},L) by A5, YELLOW_0:35; hence b <= a by A4, YELLOW_0:39; ::_thesis: verum end; theorem Th32: :: WAYBEL12:32 for L being Semilattice for F being Filter of L for G being GeneratorSet of F for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds rng g is GeneratorSet of F proof let L be Semilattice; ::_thesis: for F being Filter of L for G being GeneratorSet of F for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds rng g is GeneratorSet of F let F be Filter of L; ::_thesis: for G being GeneratorSet of F for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds rng g is GeneratorSet of F let G be GeneratorSet of F; ::_thesis: for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds rng g is GeneratorSet of F let f, g be Function of NAT, the carrier of L; ::_thesis: ( rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies rng g is GeneratorSet of F ) assume that A1: rng f = G and A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; ::_thesis: rng g is GeneratorSet of F A3: rng g is_coarser_than F proof let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in rng g or ex b1 being Element of the carrier of L st ( b1 in F & b1 <= a ) ) assume a in rng g ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in F & b1 <= a ) then consider n being set such that A4: n in dom g and A5: g . n = a by FUNCT_1:def_3; reconsider n = n as Element of NAT by A4; reconsider Y = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1; A6: Y c= G proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Y or q in G ) assume q in Y ; ::_thesis: q in G then A7: ex m being Element of NAT st ( q = f . m & m <= n ) ; dom f = NAT by FUNCT_2:def_1; hence q in G by A1, A7, FUNCT_1:def_3; ::_thesis: verum end; G c= F by Lm4; then Y c= F by A6, XBOOLE_1:1; then A8: "/\" (Y,L) in F by WAYBEL_0:43; g . n = "/\" (Y,L) by A2; hence ex b being Element of L st ( b in F & b <= a ) by A5, A8; ::_thesis: verum end; g . 0 in rng g by FUNCT_2:4; hence rng g is GeneratorSet of F by A1, A2, A3, Th30, Th31; ::_thesis: verum end; begin theorem Th33: :: WAYBEL12:33 for L being lower-bounded continuous LATTICE for V being upper Open Subset of L for F being Filter of L for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds ex O being Open Filter of L st ( O c= V & v in O & F c= O ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L for F being Filter of L for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds ex O being Open Filter of L st ( O c= V & v in O & F c= O ) let V be upper Open Subset of L; ::_thesis: for F being Filter of L for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds ex O being Open Filter of L st ( O c= V & v in O & F c= O ) let F be Filter of L; ::_thesis: for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds ex O being Open Filter of L st ( O c= V & v in O & F c= O ) let v be Element of L; ::_thesis: ( V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable implies ex O being Open Filter of L st ( O c= V & v in O & F c= O ) ) assume that A1: V "/\" F c= V and A2: v in V ; ::_thesis: ( for A being non empty GeneratorSet of F holds not A is countable or ex O being Open Filter of L st ( O c= V & v in O & F c= O ) ) reconsider V1 = V as non empty upper Open Subset of L by A2; reconsider v1 = v as Element of V1 by A2; reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th23, Th24, Th25; given A being non empty GeneratorSet of F such that A3: A is countable ; ::_thesis: ex O being Open Filter of L st ( O c= V & v in O & F c= O ) consider f being Function of NAT,A such that A4: rng f = A by A3, CARD_3:96; reconsider f = f as Function of NAT, the carrier of L by FUNCT_2:7; deffunc H1( Element of NAT ) -> Element of the carrier of L = "/\" ( { (f . m) where m is Element of NAT : m <= \$1 } ,L); consider g being Function of NAT, the carrier of L such that A5: for n being Element of NAT holds g . n = H1(n) from FUNCT_2:sch_4(); defpred S1[ Element of NAT , set , set ] means ex x1, y1 being Element of V1 ex z1 being Element of L st ( x1 = \$2 & y1 = \$3 & z1 = g . (\$1 + 1) & y1 << x1 "/\" z1 ); A6: dom g = NAT by FUNCT_2:def_1; then reconsider AA = rng g as non empty Subset of L by RELAT_1:42; A7: AA is GeneratorSet of F by A4, A5, Th32; A8: F c= G proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F or q in G ) assume A9: q in F ; ::_thesis: q in G then reconsider s = q as Element of L ; A10: V "/\" {s} = { (s "/\" t) where t is Element of L : t in V } by YELLOW_4:42; V "/\" {s} c= V proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in V "/\" {s} or w in V ) assume w in V "/\" {s} ; ::_thesis: w in V then consider t being Element of L such that A11: w = s "/\" t and A12: t in V by A10; t "/\" s in V "/\" F by A9, A12; hence w in V by A1, A11; ::_thesis: verum end; hence q in G ; ::_thesis: verum end; A13: for n being Element of NAT for x being Element of V1 ex y being Element of V1 st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of V1 ex y being Element of V1 st S1[n,x,y] let x be Element of V1; ::_thesis: ex y being Element of V1 st S1[n,x,y] AA c= F by A7, Lm4; then A14: AA c= G by A8, XBOOLE_1:1; g . (n + 1) in AA by A6, FUNCT_1:def_3; then g . (n + 1) in G by A14; then consider g1 being Element of L such that A15: g . (n + 1) = g1 and A16: V "/\" {g1} c= V ; g1 in {g1} by TARSKI:def_1; then x "/\" g1 in V "/\" {g1} ; then ex y1 being Element of L st ( y1 in V & y1 << x "/\" g1 ) by A16, WAYBEL_6:def_1; hence ex y being Element of V1 st S1[n,x,y] by A15; ::_thesis: verum end; consider h being Function of NAT,V1 such that A17: h . 0 = v1 and A18: for n being Element of NAT holds S1[n,h . n,h . (n + 1)] from RECDEF_1:sch_2(A13); A19: dom h = NAT by FUNCT_2:def_1; then A20: h . 0 in rng h by FUNCT_1:def_3; then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1; set O = uparrow (fininfs R); A21: R c= uparrow (fininfs R) by WAYBEL_0:62; A22: for x, y being Element of L for n being Element of NAT st h . n = x & h . (n + 1) = y holds y <= x proof let x, y be Element of L; ::_thesis: for n being Element of NAT st h . n = x & h . (n + 1) = y holds y <= x let n be Element of NAT ; ::_thesis: ( h . n = x & h . (n + 1) = y implies y <= x ) assume A23: ( h . n = x & h . (n + 1) = y ) ; ::_thesis: y <= x consider x1, y1 being Element of V1, z1 being Element of L such that A24: ( x1 = h . n & y1 = h . (n + 1) ) and z1 = g . (n + 1) and A25: y1 << x1 "/\" z1 by A18; A26: x1 "/\" z1 <= x1 by YELLOW_0:23; y1 <= x1 "/\" z1 by A25, WAYBEL_3:1; hence y <= x by A23, A24, A26, ORDERS_2:3; ::_thesis: verum end; A27: for x, y being Element of L for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds y <= x proof defpred S2[ Element of NAT ] means for a being Element of NAT for s, t being Element of L st t = h . a & s = h . \$1 & a <= \$1 holds s <= t; A28: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A29: for j being Element of NAT for s, t being Element of L st t = h . j & s = h . k & j <= k holds s <= t ; ::_thesis: S2[k + 1] h . k in R by A19, FUNCT_1:def_3; then reconsider s = h . k as Element of L ; let a be Element of NAT ; ::_thesis: for s, t being Element of L st t = h . a & s = h . (k + 1) & a <= k + 1 holds s <= t let c, d be Element of L; ::_thesis: ( d = h . a & c = h . (k + 1) & a <= k + 1 implies c <= d ) assume that A30: d = h . a and A31: c = h . (k + 1) and A32: a <= k + 1 ; ::_thesis: c <= d A33: c <= s by A22, A31; percases ( a <= k or a = k + 1 ) by A32, NAT_1:8; suppose a <= k ; ::_thesis: c <= d then s <= d by A29, A30; hence c <= d by A33, ORDERS_2:3; ::_thesis: verum end; suppose a = k + 1 ; ::_thesis: c <= d hence c <= d by A30, A31; ::_thesis: verum end; end; end; A34: S2[ 0 ] by NAT_1:3; A35: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A34, A28); let x, y be Element of L; ::_thesis: for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds y <= x let n, m be Element of NAT ; ::_thesis: ( h . n = x & h . m = y & n <= m implies y <= x ) assume ( h . n = x & h . m = y & n <= m ) ; ::_thesis: y <= x hence y <= x by A35; ::_thesis: verum end; A36: for x, y being Element of L st x in R & y in R & not x <= y holds y <= x proof let x, y be Element of L; ::_thesis: ( x in R & y in R & not x <= y implies y <= x ) assume that A37: x in R and A38: y in R ; ::_thesis: ( x <= y or y <= x ) consider m being set such that A39: m in dom h and A40: y = h . m by A38, FUNCT_1:def_3; reconsider m = m as Element of NAT by A39; consider n being set such that A41: n in dom h and A42: x = h . n by A37, FUNCT_1:def_3; reconsider n = n as Element of NAT by A41; percases ( m <= n or n <= m ) ; suppose m <= n ; ::_thesis: ( x <= y or y <= x ) hence ( x <= y or y <= x ) by A27, A42, A40; ::_thesis: verum end; suppose n <= m ; ::_thesis: ( x <= y or y <= x ) hence ( x <= y or y <= x ) by A27, A42, A40; ::_thesis: verum end; end; end; A43: uparrow (fininfs R) is Open proof let x be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in uparrow (fininfs R) or ex b1 being Element of the carrier of L st ( b1 in uparrow (fininfs R) & b1 is_way_below x ) ) assume x in uparrow (fininfs R) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in uparrow (fininfs R) & b1 is_way_below x ) then consider y being Element of L such that A44: y <= x and A45: y in fininfs R by WAYBEL_0:def_16; consider Y being finite Subset of R such that A46: y = "/\" (Y,L) and ex_inf_of Y,L by A45; percases ( Y <> {} or Y = {} ) ; suppose Y <> {} ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in uparrow (fininfs R) & b1 is_way_below x ) then y in Y by A36, A46, Th27; then consider n being set such that A47: n in dom h and A48: h . n = y by FUNCT_1:def_3; reconsider n = n as Element of NAT by A47; consider x1, y1 being Element of V1, z1 being Element of L such that A49: x1 = h . n and A50: y1 = h . (n + 1) and z1 = g . (n + 1) and A51: y1 << x1 "/\" z1 by A18; take y1 ; ::_thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x ) y1 in R by A19, A50, FUNCT_1:def_3; hence y1 in uparrow (fininfs R) by A21; ::_thesis: y1 is_way_below x x1 "/\" z1 <= x1 by YELLOW_0:23; then y1 << x1 by A51, WAYBEL_3:2; hence y1 is_way_below x by A44, A48, A49, WAYBEL_3:2; ::_thesis: verum end; supposeA52: Y = {} ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in uparrow (fininfs R) & b1 is_way_below x ) consider b being set such that A53: b in R by XBOOLE_0:def_1; reconsider b = b as Element of L by A53; consider n being set such that A54: n in dom h and h . n = b by A53, FUNCT_1:def_3; reconsider n = n as Element of NAT by A54; A55: x <= Top L by YELLOW_0:45; consider x1, y1 being Element of V1, z1 being Element of L such that x1 = h . n and A56: y1 = h . (n + 1) and z1 = g . (n + 1) and A57: y1 << x1 "/\" z1 by A18; y = Top L by A46, A52, YELLOW_0:def_12; then x = Top L by A44, A55, ORDERS_2:2; then A58: x1 <= x by YELLOW_0:45; take y1 ; ::_thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x ) y1 in R by A19, A56, FUNCT_1:def_3; hence y1 in uparrow (fininfs R) by A21; ::_thesis: y1 is_way_below x x1 "/\" z1 <= x1 by YELLOW_0:23; then y1 << x1 by A57, WAYBEL_3:2; hence y1 is_way_below x by A58, WAYBEL_3:2; ::_thesis: verum end; end; end; A59: for n being Element of NAT for a, b being Element of L st a = g . n & b = g . (n + 1) holds b <= a proof let n be Element of NAT ; ::_thesis: for a, b being Element of L st a = g . n & b = g . (n + 1) holds b <= a let a, b be Element of L; ::_thesis: ( a = g . n & b = g . (n + 1) implies b <= a ) assume A60: ( a = g . n & b = g . (n + 1) ) ; ::_thesis: b <= a reconsider gn = { (f . m) where m is Element of NAT : m <= n } , gn1 = { (f . k) where k is Element of NAT : k <= n + 1 } as non empty finite Subset of L by Lm1; A61: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55; A62: gn c= gn1 proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in gn or i in gn1 ) assume i in gn ; ::_thesis: i in gn1 then consider k being Element of NAT such that A63: i = f . k and A64: k <= n ; k <= n + 1 by A64, NAT_1:12; hence i in gn1 by A63; ::_thesis: verum end; ( a = "/\" (gn,L) & b = "/\" (gn1,L) ) by A5, A60; hence b <= a by A61, A62, YELLOW_0:35; ::_thesis: verum end; A65: AA is_coarser_than R proof let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in AA or ex b1 being Element of the carrier of L st ( b1 in R & b1 <= a ) ) assume a in AA ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in R & b1 <= a ) then consider x being set such that A66: x in dom g and A67: g . x = a by FUNCT_1:def_3; reconsider x = x as Element of NAT by A66; consider x1, y1 being Element of V1, z1 being Element of L such that x1 = h . x and A68: y1 = h . (x + 1) and A69: z1 = g . (x + 1) and A70: y1 << x1 "/\" z1 by A18; ( x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 ) by A70, WAYBEL_3:1, YELLOW_0:23; then A71: y1 <= z1 by ORDERS_2:3; A72: h . (x + 1) in R by A19, FUNCT_1:def_3; z1 <= a by A59, A67, A69; hence ex b being Element of L st ( b in R & b <= a ) by A68, A72, A71, ORDERS_2:3; ::_thesis: verum end; reconsider O = uparrow (fininfs R) as Open Filter of L by A43; R is_coarser_than O by A21, Th16; then A73: AA c= O by A65, YELLOW_4:7, YELLOW_4:8; take O ; ::_thesis: ( O c= V & v in O & F c= O ) thus O c= V ::_thesis: ( v in O & F c= O ) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O or q in V ) assume q in O ; ::_thesis: q in V then reconsider q = q as Element of O ; consider y being Element of L such that A74: y <= q and A75: y in fininfs R by WAYBEL_0:def_16; consider Y being finite Subset of R such that A76: y = "/\" (Y,L) and ex_inf_of Y,L by A75; percases ( Y <> {} or Y = {} ) ; suppose Y <> {} ; ::_thesis: q in V then y in Y by A36, A76, Th27; then consider n being set such that A77: n in dom h and A78: h . n = y by FUNCT_1:def_3; reconsider n = n as Element of NAT by A77; ex x1, y1 being Element of V1 ex z1 being Element of L st ( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A18; hence q in V by A74, A78, WAYBEL_0:def_20; ::_thesis: verum end; supposeA79: Y = {} ; ::_thesis: q in V A80: q <= Top L by YELLOW_0:45; y = Top L by A76, A79, YELLOW_0:def_12; then q = Top L by A74, A80, ORDERS_2:2; hence q in V by Th8; ::_thesis: verum end; end; end; thus v in O by A17, A20, A21; ::_thesis: F c= O uparrow (fininfs AA) = F by A7, Def3; hence F c= O by A73, WAYBEL_0:62; ::_thesis: verum end; theorem Th34: :: WAYBEL12:34 for L being lower-bounded continuous LATTICE for V being upper Open Subset of L for N being non empty countable Subset of L for v being Element of L st V "/\" N c= V & v in V holds ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L for N being non empty countable Subset of L for v being Element of L st V "/\" N c= V & v in V holds ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) let V be upper Open Subset of L; ::_thesis: for N being non empty countable Subset of L for v being Element of L st V "/\" N c= V & v in V holds ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) let N be non empty countable Subset of L; ::_thesis: for v being Element of L st V "/\" N c= V & v in V holds ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) let v be Element of L; ::_thesis: ( V "/\" N c= V & v in V implies ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) ) assume that A1: V "/\" N c= V and A2: v in V ; ::_thesis: ex O being Open Filter of L st ( {v} "/\" N c= O & O c= V & v in O ) reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th23, Th24, Th25; A3: N c= G proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in N or q in G ) assume A4: q in N ; ::_thesis: q in G then reconsider q1 = q as Element of L ; A5: {q1} "/\" V = { (q1 "/\" y) where y is Element of L : y in V } by YELLOW_4:42; V "/\" {q1} c= V proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in V "/\" {q1} or t in V ) assume t in V "/\" {q1} ; ::_thesis: t in V then consider y being Element of L such that A6: t = q1 "/\" y and A7: y in V by A5; q1 "/\" y in N "/\" V by A4, A7; hence t in V by A1, A6; ::_thesis: verum end; hence q in G ; ::_thesis: verum end; N is GeneratorSet of uparrow (fininfs N) by Def3; then consider F being Filter of L such that A8: N is GeneratorSet of F ; F = uparrow (fininfs N) by A8, Def3; then A9: F c= G by A3, WAYBEL_0:62; V "/\" F c= V proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in V "/\" F or q in V ) assume q in V "/\" F ; ::_thesis: q in V then consider d, f being Element of L such that A10: q = d "/\" f and A11: d in V and A12: f in F ; f in G by A9, A12; then consider x being Element of L such that A13: f = x and A14: V "/\" {x} c= V ; x in {x} by TARSKI:def_1; then d "/\" f in V "/\" {x} by A11, A13; hence q in V by A10, A14; ::_thesis: verum end; then consider O being Open Filter of L such that A15: O c= V and A16: v in O and A17: F c= O by A2, A8, Th33; take O ; ::_thesis: ( {v} "/\" N c= O & O c= V & v in O ) A18: {v} "/\" N = { (v "/\" n) where n is Element of L : n in N } by YELLOW_4:42; thus {v} "/\" N c= O ::_thesis: ( O c= V & v in O ) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {v} "/\" N or q in O ) assume q in {v} "/\" N ; ::_thesis: q in O then consider n being Element of L such that A19: q = v "/\" n and A20: n in N by A18; N c= F by A8, Lm4; then N c= O by A17, XBOOLE_1:1; then v "/\" n in O "/\" O by A16, A20; hence q in O by A19, Th21; ::_thesis: verum end; thus ( O c= V & v in O ) by A15, A16; ::_thesis: verum end; theorem Th35: :: WAYBEL12:35 for L being lower-bounded continuous LATTICE for V being upper Open Subset of L for N being non empty countable Subset of L for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L for N being non empty countable Subset of L for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) let V be upper Open Subset of L; ::_thesis: for N being non empty countable Subset of L for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) let N be non empty countable Subset of L; ::_thesis: for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) let x, y be Element of L; ::_thesis: ( V "/\" N c= V & y in V & not x in V implies ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) ) assume that A1: ( V "/\" N c= V & y in V ) and A2: not x in V ; ::_thesis: ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) consider O being Open Filter of L such that A3: {y} "/\" N c= O and A4: O c= V and y in O by A1, Th34; ( uparrow O c= O & O c= uparrow O ) by WAYBEL_0:16, WAYBEL_0:24; then uparrow O = O by XBOOLE_0:def_10; then A5: uparrow ({y} "/\" N) c= O by A3, YELLOW_3:7; not x in O by A2, A4; then x in O ` by XBOOLE_0:def_5; then consider p being Element of L such that A6: x <= p and A7: p is_maximal_in O ` by WAYBEL_6:9; reconsider p = p as irreducible Element of L by A7, WAYBEL_6:13; take p ; ::_thesis: ( x <= p & not p in uparrow ({y} "/\" N) ) thus x <= p by A6; ::_thesis: not p in uparrow ({y} "/\" N) p in O ` by A7, WAYBEL_4:55; hence not p in uparrow ({y} "/\" N) by A5, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th36: :: WAYBEL12:36 for L being lower-bounded continuous LATTICE for x being Element of L for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x ) holds for y being Element of L st not y <= x holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for x being Element of L for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x ) holds for y being Element of L st not y <= x holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) let x be Element of L; ::_thesis: for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x ) holds for y being Element of L st not y <= x holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) let N be non empty countable Subset of L; ::_thesis: ( ( for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x ) implies for y being Element of L st not y <= x holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) ) assume A1: for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x ; ::_thesis: for y being Element of L st not y <= x holds ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) set V = (downarrow x) ` ; A2: ((downarrow x) `) "/\" N c= (downarrow x) ` proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ((downarrow x) `) "/\" N or q in (downarrow x) ` ) assume q in ((downarrow x) `) "/\" N ; ::_thesis: q in (downarrow x) ` then consider v, n being Element of L such that A3: q = v "/\" n and A4: v in (downarrow x) ` and A5: n in N ; not v in downarrow x by A4, XBOOLE_0:def_5; then not v <= x by WAYBEL_0:17; then not v "/\" n <= x by A1, A5; then not v "/\" n in downarrow x by WAYBEL_0:17; hence q in (downarrow x) ` by A3, XBOOLE_0:def_5; ::_thesis: verum end; x <= x ; then x in downarrow x by WAYBEL_0:17; then A6: not x in (downarrow x) ` by XBOOLE_0:def_5; let y be Element of L; ::_thesis: ( not y <= x implies ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) ) assume not y <= x ; ::_thesis: ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) then not y in downarrow x by WAYBEL_0:17; then y in (downarrow x) ` by XBOOLE_0:def_5; hence ex p being irreducible Element of L st ( x <= p & not p in uparrow ({y} "/\" N) ) by A2, A6, Th35; ::_thesis: verum end; definition let L be non empty RelStr ; let u be Element of L; attru is dense means :Def4: :: WAYBEL12:def 4 for v being Element of L st v <> Bottom L holds u "/\" v <> Bottom L; end; :: deftheorem Def4 defines dense WAYBEL12:def_4_:_ for L being non empty RelStr for u being Element of L holds ( u is dense iff for v being Element of L st v <> Bottom L holds u "/\" v <> Bottom L ); registration let L be upper-bounded Semilattice; cluster Top L -> dense ; coherence Top L is dense proof let v be Element of L; :: according to WAYBEL12:def_4 ::_thesis: ( v <> Bottom L implies (Top L) "/\" v <> Bottom L ) assume v <> Bottom L ; ::_thesis: (Top L) "/\" v <> Bottom L hence (Top L) "/\" v <> Bottom L by WAYBEL_1:4; ::_thesis: verum end; end; registration let L be upper-bounded Semilattice; cluster dense for Element of the carrier of L; existence ex b1 being Element of L st b1 is dense proof take Top L ; ::_thesis: Top L is dense thus Top L is dense ; ::_thesis: verum end; end; theorem :: WAYBEL12:37 for L being non trivial bounded Semilattice for x being Element of L st x is dense holds x <> Bottom L proof let L be non trivial bounded Semilattice; ::_thesis: for x being Element of L st x is dense holds x <> Bottom L let x be Element of L; ::_thesis: ( x is dense implies x <> Bottom L ) assume A1: x is dense ; ::_thesis: x <> Bottom L Top L <> Bottom L by WAYBEL_7:3; then x "/\" (Top L) <> Bottom L by A1, Def4; hence x <> Bottom L by WAYBEL_1:4; ::_thesis: verum end; definition let L be non empty RelStr ; let D be Subset of L; attrD is dense means :Def5: :: WAYBEL12:def 5 for d being Element of L st d in D holds d is dense ; end; :: deftheorem Def5 defines dense WAYBEL12:def_5_:_ for L being non empty RelStr for D being Subset of L holds ( D is dense iff for d being Element of L st d in D holds d is dense ); theorem Th38: :: WAYBEL12:38 for L being upper-bounded Semilattice holds {(Top L)} is dense proof let L be upper-bounded Semilattice; ::_thesis: {(Top L)} is dense let d be Element of L; :: according to WAYBEL12:def_5 ::_thesis: ( d in {(Top L)} implies d is dense ) assume d in {(Top L)} ; ::_thesis: d is dense hence d is dense by TARSKI:def_1; ::_thesis: verum end; registration let L be upper-bounded Semilattice; cluster non empty finite countable dense for Element of bool the carrier of L; existence ex b1 being Subset of L st ( not b1 is empty & b1 is finite & b1 is countable & b1 is dense ) proof take {(Top L)} ; ::_thesis: ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable & {(Top L)} is dense ) thus ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable ) ; ::_thesis: {(Top L)} is dense thus {(Top L)} is dense by Th38; ::_thesis: verum end; end; theorem Th39: :: WAYBEL12:39 for L being lower-bounded continuous LATTICE for D being non empty countable dense Subset of L for u being Element of L st u <> Bottom L holds ex p being irreducible Element of L st ( p <> Top L & not p in uparrow ({u} "/\" D) ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for D being non empty countable dense Subset of L for u being Element of L st u <> Bottom L holds ex p being irreducible Element of L st ( p <> Top L & not p in uparrow ({u} "/\" D) ) let D be non empty countable dense Subset of L; ::_thesis: for u being Element of L st u <> Bottom L holds ex p being irreducible Element of L st ( p <> Top L & not p in uparrow ({u} "/\" D) ) let u be Element of L; ::_thesis: ( u <> Bottom L implies ex p being irreducible Element of L st ( p <> Top L & not p in uparrow ({u} "/\" D) ) ) assume A1: u <> Bottom L ; ::_thesis: ex p being irreducible Element of L st ( p <> Top L & not p in uparrow ({u} "/\" D) ) A2: for d, y being Element of L st not y <= Bottom L & d in D holds not y "/\" d <= Bottom L proof let d, y be Element of L; ::_thesis: ( not y <= Bottom L & d in D implies not y "/\" d <= Bottom L ) assume A3: not y <= Bottom L ; ::_thesis: ( not d in D or not y "/\" d <= Bottom L ) assume d in D ; ::_thesis: not y "/\" d <= Bottom L then d is dense by Def5; then A4: y "/\" d <> Bottom L by A3, Def4; Bottom L <= y "/\" d by YELLOW_0:44; hence not y "/\" d <= Bottom L by A4, ORDERS_2:2; ::_thesis: verum end; Bottom L <= u by YELLOW_0:44; then not u <= Bottom L by A1, ORDERS_2:2; then consider p being irreducible Element of L such that Bottom L <= p and A5: not p in uparrow ({u} "/\" D) by A2, Th36; take p ; ::_thesis: ( p <> Top L & not p in uparrow ({u} "/\" D) ) thus p <> Top L by A5, Th9; ::_thesis: not p in uparrow ({u} "/\" D) thus not p in uparrow ({u} "/\" D) by A5; ::_thesis: verum end; theorem Th40: :: WAYBEL12:40 for T being non empty TopSpace for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B & B ` is irreducible holds A is irreducible proof let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B & B ` is irreducible holds A is irreducible let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B & B ` is irreducible holds A is irreducible let B be Subset of T; ::_thesis: ( A = B & B ` is irreducible implies A is irreducible ) assume A1: A = B ; ::_thesis: ( not B ` is irreducible or A is irreducible ) assume that ( not B ` is empty & B ` is closed ) and A2: for S1, S2 being Subset of T st S1 is closed & S2 is closed & B ` = S1 \/ S2 & not S1 = B ` holds S2 = B ` ; :: according to YELLOW_8:def_3 ::_thesis: A is irreducible let x, y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_2 ::_thesis: ( not A = x "/\" y or x = A or y = A ) assume A3: A = x "/\" y ; ::_thesis: ( x = A or y = A ) A4: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1; then ( x in the topology of T & y in the topology of T ) ; then reconsider x1 = x, y1 = y as Subset of T ; A5: y1 is open by A4, PRE_TOPC:def_2; then A6: y1 ` is closed ; A7: x1 is open by A4, PRE_TOPC:def_2; then x1 /\ y1 is open by A5; then x /\ y in the topology of T by PRE_TOPC:def_2; then A = x /\ y by A3, YELLOW_1:9; then A8: B ` = (x1 `) \/ (y1 `) by A1, XBOOLE_1:54; x1 ` is closed by A7; then ( x1 ` = B ` or y1 ` = B ` ) by A2, A6, A8; hence ( x = A or y = A ) by A1, TOPS_1:1; ::_thesis: verum end; theorem Th41: :: WAYBEL12:41 for T being non empty TopSpace for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds ( A is irreducible iff B ` is irreducible ) proof let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds ( A is irreducible iff B ` is irreducible ) let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds ( A is irreducible iff B ` is irreducible ) let B be Subset of T; ::_thesis: ( A = B & A <> Top (InclPoset the topology of T) implies ( A is irreducible iff B ` is irreducible ) ) assume that A1: A = B and A2: A <> Top (InclPoset the topology of T) ; ::_thesis: ( A is irreducible iff B ` is irreducible ) A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1; hereby ::_thesis: ( B ` is irreducible implies A is irreducible ) assume A4: A is irreducible ; ::_thesis: B ` is irreducible thus B ` is irreducible ::_thesis: verum proof A5: B <> the carrier of T by A1, A2, YELLOW_1:24; now__::_thesis:_not_the_carrier_of_T_\_B_=_{} assume the carrier of T \ B = {} ; ::_thesis: contradiction then the carrier of T c= B by XBOOLE_1:37; hence contradiction by A5, XBOOLE_0:def_10; ::_thesis: verum end; hence not B ` is empty ; :: according to YELLOW_8:def_3 ::_thesis: ( B ` is closed & ( for b1, b2 being Element of bool the carrier of T holds ( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = B ` ) ) ) (B `) ` is open by A1, A3, PRE_TOPC:def_2; hence B ` is closed ; ::_thesis: for b1, b2 being Element of bool the carrier of T holds ( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = B ` ) let S1, S2 be Subset of T; ::_thesis: ( not S1 is closed or not S2 is closed or not B ` = S1 \/ S2 or S1 = B ` or S2 = B ` ) assume that A6: ( S1 is closed & S2 is closed ) and A7: B ` = S1 \/ S2 ; ::_thesis: ( S1 = B ` or S2 = B ` ) A8: ( S1 ` is open & S2 ` is open ) by A6; then reconsider s1 = S1 ` , s2 = S2 ` as Element of (InclPoset the topology of T) by A3, PRE_TOPC:def_2; (S1 `) /\ (S2 `) is open by A8; then A9: s1 /\ s2 in the topology of T by PRE_TOPC:def_2; B = (S1 \/ S2) ` by A7 .= (S1 `) /\ (S2 `) by XBOOLE_1:53 ; then A = s1 "/\" s2 by A1, A9, YELLOW_1:9; then ( A = s1 or A = s2 ) by A4, WAYBEL_6:def_2; hence ( S1 = B ` or S2 = B ` ) by A1; ::_thesis: verum end; end; thus ( B ` is irreducible implies A is irreducible ) by A1, Th40; ::_thesis: verum end; theorem Th42: :: WAYBEL12:42 for T being non empty TopSpace for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B holds ( A is dense iff B is everywhere_dense ) proof let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T) for B being Subset of T st A = B holds ( A is dense iff B is everywhere_dense ) let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B holds ( A is dense iff B is everywhere_dense ) let B be Subset of T; ::_thesis: ( A = B implies ( A is dense iff B is everywhere_dense ) ) assume A1: A = B ; ::_thesis: ( A is dense iff B is everywhere_dense ) A2: Bottom (InclPoset the topology of T) = {} by PRE_TOPC:1, YELLOW_1:13; A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1; then A4: B is open by A1, PRE_TOPC:def_2; hereby ::_thesis: ( B is everywhere_dense implies A is dense ) assume A5: A is dense ; ::_thesis: B is everywhere_dense for Q being Subset of T st Q <> {} & Q is open holds B meets Q proof let Q be Subset of T; ::_thesis: ( Q <> {} & Q is open implies B meets Q ) assume that A6: Q <> {} and A7: Q is open ; ::_thesis: B meets Q reconsider q = Q as Element of (InclPoset the topology of T) by A3, A7, PRE_TOPC:def_2; B /\ Q is open by A4, A7; then A8: A /\ q in the topology of T by A1, PRE_TOPC:def_2; A "/\" q <> Bottom (InclPoset the topology of T) by A2, A5, A6, Def4; then B /\ Q <> {} by A1, A2, A8, YELLOW_1:9; hence B meets Q by XBOOLE_0:def_7; ::_thesis: verum end; then B is dense by TOPS_1:45; hence B is everywhere_dense by A4, TOPS_3:36; ::_thesis: verum end; assume B is everywhere_dense ; ::_thesis: A is dense then A9: B is dense by TOPS_3:33; let v be Element of (InclPoset the topology of T); :: according to WAYBEL12:def_4 ::_thesis: ( v <> Bottom (InclPoset the topology of T) implies A "/\" v <> Bottom (InclPoset the topology of T) ) assume A10: v <> Bottom (InclPoset the topology of T) ; ::_thesis: A "/\" v <> Bottom (InclPoset the topology of T) v in the topology of T by A3; then reconsider V = v as Subset of T ; A11: V is open by A3, PRE_TOPC:def_2; B is open by A1, A3, PRE_TOPC:def_2; then B /\ V is open by A11; then A12: B /\ V in the topology of T by PRE_TOPC:def_2; B meets V by A2, A9, A10, A11, TOPS_1:45; then B /\ V <> {} by XBOOLE_0:def_7; hence A "/\" v <> Bottom (InclPoset the topology of T) by A1, A2, A12, YELLOW_1:9; ::_thesis: verum end; theorem Th43: :: WAYBEL12:43 for T being non empty TopSpace st T is locally-compact holds for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds for O being non empty Subset of T st O is open holds ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V proof let T be non empty TopSpace; ::_thesis: ( T is locally-compact implies for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds for O being non empty Subset of T st O is open holds ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V ) assume T is locally-compact ; ::_thesis: for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds for O being non empty Subset of T st O is open holds ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V then reconsider L = InclPoset the topology of T as bounded continuous LATTICE by WAYBEL_3:42; A1: the carrier of L = the topology of T by YELLOW_1:1; let D be countable Subset-Family of T; ::_thesis: ( not D is empty & D is dense & D is open implies for O being non empty Subset of T st O is open holds ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V ) assume A2: ( not D is empty & D is dense & D is open ) ; ::_thesis: for O being non empty Subset of T st O is open holds ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V consider I being set such that A3: I in D by A2, XBOOLE_0:def_1; reconsider I = I as Subset of T by A3; I is open by A2, A3, TOPS_2:def_1; then reconsider i = I as Element of L by A1, PRE_TOPC:def_2; set D1 = { d where d is Element of L : ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) } ; { d where d is Element of L : ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { d where d is Element of L : ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) } or q in the carrier of L ) assume q in { d where d is Element of L : ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) } ; ::_thesis: q in the carrier of L then ex d being Element of L st ( q = d & ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) ) ; hence q in the carrier of L ; ::_thesis: verum end; then reconsider D1 = { d where d is Element of L : ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) } as Subset of L ; A4: D1 c= D proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 or q in D ) assume q in D1 ; ::_thesis: q in D then ex d being Element of L st ( q = d & ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) ) ; hence q in D ; ::_thesis: verum end; A5: D1 is dense proof let q be Element of L; :: according to WAYBEL12:def_5 ::_thesis: ( q in D1 implies q is dense ) assume q in D1 ; ::_thesis: q is dense then ex d being Element of L st ( q = d & ex d1 being Subset of T st ( d1 in D & d1 = d & d is dense ) ) ; hence q is dense ; ::_thesis: verum end; let O be non empty Subset of T; ::_thesis: ( O is open implies ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V ) assume A6: O is open ; ::_thesis: ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V reconsider u = O as Element of L by A6, A1, PRE_TOPC:def_2; ( I is open & I is dense ) by A2, A3, Def2, TOPS_2:def_1; then I is everywhere_dense by TOPS_3:36; then i is dense by Th42; then ( u <> Bottom L & i in D1 ) by A3, PRE_TOPC:1, YELLOW_1:13; then consider p being irreducible Element of L such that A7: p <> Top L and A8: not p in uparrow ({u} "/\" D1) by A4, A5, Th39; p in the topology of T by A1; then reconsider P = p as Subset of T ; reconsider A = P ` as irreducible Subset of T by A7, Th41; take A ; ::_thesis: for V being Subset of T st V in D holds A /\ O meets V let V be Subset of T; ::_thesis: ( V in D implies A /\ O meets V ) assume A9: V in D ; ::_thesis: A /\ O meets V then A10: V is open by A2, TOPS_2:def_1; then reconsider v = V as Element of L by A1, PRE_TOPC:def_2; A11: for d1 being Element of L st d1 in D1 holds not u "/\" d1 <= p proof A12: u in {u} by TARSKI:def_1; let d1 be Element of L; ::_thesis: ( d1 in D1 implies not u "/\" d1 <= p ) assume d1 in D1 ; ::_thesis: not u "/\" d1 <= p then u "/\" d1 in {u} "/\" D1 by A12; hence not u "/\" d1 <= p by A8, WAYBEL_0:def_16; ::_thesis: verum end; V is dense by A2, A9, Def2; then V is everywhere_dense by A10, TOPS_3:36; then v is dense by Th42; then v in D1 by A9; then not u "/\" v <= p by A11; then A13: not u "/\" v c= p by YELLOW_1:3; O /\ V is open by A6, A10; then u /\ v in the topology of T by PRE_TOPC:def_2; then not O /\ V c= p by A13, YELLOW_1:9; then consider x being set such that A14: x in O /\ V and A15: not x in A ` by TARSKI:def_3; reconsider x = x as Element of T by A14; x in A by A15, XBOOLE_0:def_5; then (O /\ V) /\ A <> {} by A14, XBOOLE_0:def_4; hence (A /\ O) /\ V <> {} by XBOOLE_1:16; :: according to XBOOLE_0:def_7 ::_thesis: verum end; definition let T be non empty TopSpace; redefine attr T is Baire means :: WAYBEL12:def 6 for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ); compatibility ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ) proof set D = bool the carrier of T; hereby ::_thesis: ( ( for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ) implies T is Baire ) assume A1: T is Baire ; ::_thesis: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) thus for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ::_thesis: verum proof let F be Subset-Family of T; ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) implies ex I being Subset of T st ( I = Intersect F & I is dense ) ) assume that A2: F is countable and A3: for S being Subset of T st S in F holds ( S is open & S is dense ) ; ::_thesis: ex I being Subset of T st ( I = Intersect F & I is dense ) for S being Subset of T st S in F holds S is everywhere_dense proof let S be Subset of T; ::_thesis: ( S in F implies S is everywhere_dense ) assume S in F ; ::_thesis: S is everywhere_dense then ( S is open & S is dense ) by A3; hence S is everywhere_dense by TOPS_3:36; ::_thesis: verum end; hence ex I being Subset of T st ( I = Intersect F & I is dense ) by A1, A2, YELLOW_8:def_2; ::_thesis: verum end; end; assume A4: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ; ::_thesis: T is Baire deffunc H1( Element of bool the carrier of T) -> Element of bool the carrier of T = Int \$1; let F be Subset-Family of T; :: according to YELLOW_8:def_2 ::_thesis: ( not F is countable or ex b1 being Element of bool the carrier of T st ( b1 in F & not b1 is everywhere_dense ) or ex b1 being Element of bool the carrier of T st ( b1 = Intersect F & b1 is dense ) ) assume that A5: F is countable and A6: for S being Subset of T st S in F holds S is everywhere_dense ; ::_thesis: ex b1 being Element of bool the carrier of T st ( b1 = Intersect F & b1 is dense ) set F1 = { (Int A) where A is Subset of T : A in F } ; consider f being Function of (bool the carrier of T),(bool the carrier of T) such that A7: for x being Element of bool the carrier of T holds f . x = H1(x) from FUNCT_2:sch_4(); { (Int A) where A is Subset of T : A in F } c= f .: F proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (Int A) where A is Subset of T : A in F } or q in f .: F ) assume q in { (Int A) where A is Subset of T : A in F } ; ::_thesis: q in f .: F then consider A being Subset of T such that A8: ( q = Int A & A in F ) ; ( dom f = bool the carrier of T & f . A = Int A ) by A7, FUNCT_2:def_1; hence q in f .: F by A8, FUNCT_1:def_6; ::_thesis: verum end; then card { (Int A) where A is Subset of T : A in F } c= card F by CARD_1:66; then A9: { (Int A) where A is Subset of T : A in F } is countable by A5, Th1; reconsider J = Intersect F as Subset of T ; A10: { (Int A) where A is Subset of T : A in F } c= bool the carrier of T proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (Int A) where A is Subset of T : A in F } or q in bool the carrier of T ) assume q in { (Int A) where A is Subset of T : A in F } ; ::_thesis: q in bool the carrier of T then ex A being Subset of T st ( q = Int A & A in F ) ; hence q in bool the carrier of T ; ::_thesis: verum end; take J ; ::_thesis: ( J = Intersect F & J is dense ) thus J = Intersect F ; ::_thesis: J is dense reconsider F1 = { (Int A) where A is Subset of T : A in F } as Subset-Family of T by A10; for X being set st X in F holds Intersect F1 c= X proof let X be set ; ::_thesis: ( X in F implies Intersect F1 c= X ) assume A11: X in F ; ::_thesis: Intersect F1 c= X reconsider X1 = X as Subset of T by A11; A12: Int X1 in F1 by A11; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Intersect F1 or q in X ) assume q in Intersect F1 ; ::_thesis: q in X then ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16; hence q in X ; ::_thesis: verum end; then A13: Intersect F1 c= Intersect F by MSSUBFAM:4; now__::_thesis:_for_S_being_Subset_of_T_st_S_in_F1_holds_ (_S_is_open_&_S_is_dense_) let S be Subset of T; ::_thesis: ( S in F1 implies ( S is open & S is dense ) ) assume S in F1 ; ::_thesis: ( S is open & S is dense ) then consider A being Subset of T such that A14: S = Int A and A15: A in F ; A is everywhere_dense by A6, A15; hence ( S is open & S is dense ) by A14, TOPS_3:35; ::_thesis: verum end; then ex I being Subset of T st ( I = Intersect F1 & I is dense ) by A4, A9; hence J is dense by A13, TOPS_1:44; ::_thesis: verum end; end; :: deftheorem defines Baire WAYBEL12:def_6_:_ for T being non empty TopSpace holds ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ); theorem :: WAYBEL12:44 for T being non empty TopSpace st T is sober & T is locally-compact holds T is Baire proof let T be non empty TopSpace; ::_thesis: ( T is sober & T is locally-compact implies T is Baire ) assume A1: ( T is sober & T is locally-compact ) ; ::_thesis: T is Baire let F be Subset-Family of T; :: according to WAYBEL12:def_6 ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) implies ex I being Subset of T st ( I = Intersect F & I is dense ) ) assume that A2: F is countable and A3: for S being Subset of T st S in F holds ( S is open & S is dense ) ; ::_thesis: ex I being Subset of T st ( I = Intersect F & I is dense ) A4: F is open proof let X be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not X in F or X is open ) assume X in F ; ::_thesis: X is open hence X is open by A3; ::_thesis: verum end; for X being Subset of T st X in F holds X is dense by A3; then A5: ( F is open & F is dense ) by A4, Def2; reconsider I = Intersect F as Subset of T ; take I ; ::_thesis: ( I = Intersect F & I is dense ) thus I = Intersect F ; ::_thesis: I is dense percases ( F <> {} or F = {} ) ; supposeA6: F <> {} ; ::_thesis: I is dense for Q being Subset of T st Q <> {} & Q is open holds Intersect F meets Q proof let Q be Subset of T; ::_thesis: ( Q <> {} & Q is open implies Intersect F meets Q ) assume that A7: Q <> {} and A8: Q is open ; ::_thesis: Intersect F meets Q consider S being irreducible Subset of T such that A9: for V being Subset of T st V in F holds S /\ Q meets V by A1, A2, A5, A6, A7, A8, Th43; consider p being Point of T such that A10: p is_dense_point_of S and for q being Point of T st q is_dense_point_of S holds p = q by A1, YELLOW_8:def_5; S is closed by YELLOW_8:def_3; then A11: S = Cl {p} by A10, YELLOW_8:16; A12: for Y being set st Y in F holds ( p in Y & p in Q ) proof let Y be set ; ::_thesis: ( Y in F implies ( p in Y & p in Q ) ) assume A13: Y in F ; ::_thesis: ( p in Y & p in Q ) then reconsider Y1 = Y as Subset of T ; S /\ Q meets Y1 by A9, A13; then A14: (S /\ Q) /\ Y1 <> {} by XBOOLE_0:def_7; now__::_thesis:_p_in_Q_/\_Y1 assume not p in Q /\ Y1 ; ::_thesis: contradiction then p in (Q /\ Y1) ` by XBOOLE_0:def_5; then {p} c= (Q /\ Y1) ` by ZFMISC_1:31; then A15: Cl {p} c= Cl ((Q /\ Y1) `) by PRE_TOPC:19; Y1 is open by A3, A13; then Q /\ Y1 is open by A8; then (Q /\ Y1) ` is closed ; then S c= (Q /\ Y1) ` by A11, A15, PRE_TOPC:22; then S misses Q /\ Y1 by SUBSET_1:23; then S /\ (Q /\ Y1) = {} by XBOOLE_0:def_7; hence contradiction by A14, XBOOLE_1:16; ::_thesis: verum end; hence ( p in Y & p in Q ) by XBOOLE_0:def_4; ::_thesis: verum end; then for Y being set st Y in F holds p in Y ; then A16: p in Intersect F by SETFAM_1:43; ex Y being set st Y in F by A6, XBOOLE_0:def_1; then p in Q by A12; then (Intersect F) /\ Q <> {} by A16, XBOOLE_0:def_4; hence Intersect F meets Q by XBOOLE_0:def_7; ::_thesis: verum end; hence I is dense by TOPS_1:45; ::_thesis: verum end; suppose F = {} ; ::_thesis: I is dense then Intersect F = [#] T by SETFAM_1:def_9; hence I is dense ; ::_thesis: verum end; end; end;