:: On the Baire Category Theorem :: by Artur Korni{\l}owicz :: :: Received February 5, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ORDERS_2, FUNCT_1, NUMBERS, STRUCT_0, SUBSET_1, XXREAL_0, FINSET_1, TARSKI, CARD_1, FINSEQ_1, PRE_TOPC, RCOMP_1, SETFAM_1, TOPS_1, CARD_3, ORDINAL1, RELAT_2, WAYBEL_0, YELLOW_0, ORDINAL2, LATTICE3, LATTICES, EQREL_1, WAYBEL_6, WAYBEL_3, FINSUB_1, CARD_FIL, MSAFREE, RELAT_1, ARYTM_3, YELLOW_8, ORDERS_1, ZFMISC_1, XXREAL_2, YELLOW_1, TOPS_3, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, SETFAM_1, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1, FINSUB_1, DOMAIN_1, XXREAL_0, FUNCT_2, STRUCT_0, CARD_3, PRE_TOPC, ORDERS_2, TOPS_1, TOPS_2, TOPS_3, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8; constructors SETFAM_1, DOMAIN_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, TOPS_1, TOPS_2, TOPS_3, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8, RELSET_1, FINSEQ_1; registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XREAL_0, CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, PRE_TOPC, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_3, YELLOW_6, WAYBEL_6, WAYBEL_7, YELLOW_8, SETWISEO, CARD_3, TOPS_1, RELAT_1; requirements NUMERALS, BOOLE, SUBSET; begin definition let T be TopStruct, P be Subset of T; redefine attr P is closed means :: WAYBEL12:def 1 P` is open; end; definition let T be TopStruct, F be Subset-Family of T; attr F is dense means :: WAYBEL12:def 2 for X being Subset of T st X in F holds X is dense; end; theorem :: WAYBEL12:1 for X, Y being set st card X c= card Y & Y is countable holds X is countable; theorem :: WAYBEL12:2 for A being denumerable set holds NAT,A are_equipotent; theorem :: WAYBEL12:3 for L being non empty transitive RelStr, A, B being Subset of L st A is_finer_than B holds downarrow A c= downarrow B; theorem :: WAYBEL12:4 for L being non empty transitive RelStr, A, B being Subset of L st A is_coarser_than B holds uparrow A c= uparrow B; theorem :: WAYBEL12:5 for L being non empty Poset, D being non empty finite filtered Subset of L st ex_inf_of D,L holds inf D in D; theorem :: WAYBEL12:6 for L being lower-bounded antisymmetric non empty RelStr for X being non empty lower Subset of L holds Bottom L in X; theorem :: WAYBEL12:7 for L being lower-bounded antisymmetric non empty RelStr for X being non empty Subset of L holds Bottom L in downarrow X; theorem :: WAYBEL12:8 for L being upper-bounded antisymmetric non empty RelStr for X being non empty upper Subset of L holds Top L in X; theorem :: WAYBEL12:9 for L being upper-bounded antisymmetric non empty RelStr for X being non empty Subset of L holds Top L in uparrow X; theorem :: WAYBEL12:10 for L being lower-bounded with_infima antisymmetric RelStr for X being Subset of L holds X "/\" {Bottom L} c= {Bottom L}; theorem :: WAYBEL12:11 for L being lower-bounded with_infima antisymmetric RelStr for X being non empty Subset of L holds X "/\" {Bottom L} = {Bottom L}; theorem :: WAYBEL12:12 for L being upper-bounded with_suprema antisymmetric RelStr for X being Subset of L holds X "\/" {Top L} c= {Top L}; theorem :: WAYBEL12:13 for L being upper-bounded with_suprema antisymmetric RelStr for X being non empty Subset of L holds X "\/" {Top L} = {Top L}; theorem :: WAYBEL12:14 for L being upper-bounded Semilattice, X being Subset of L holds {Top L} "/\" X = X; theorem :: WAYBEL12:15 for L being lower-bounded with_suprema Poset, X being Subset of L holds {Bottom L} "\/" X = X; theorem :: WAYBEL12:16 for L being non empty reflexive RelStr, A, B being Subset of L st A c= B holds A is_finer_than B & A is_coarser_than B; theorem :: WAYBEL12:17 for L being antisymmetric transitive with_infima RelStr for V being Subset of L, x, y being Element of L st x <= y holds {y} "/\" V is_coarser_than {x} "/\" V; theorem :: WAYBEL12:18 for L being antisymmetric transitive with_suprema RelStr for V being Subset of L, x, y being Element of L st x <= y holds {x} "\/" V is_finer_than { y} "\/" V; theorem :: WAYBEL12:19 for L being non empty RelStr, V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds S c= V; theorem :: WAYBEL12:20 for L being non empty RelStr, V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds S c= V; theorem :: WAYBEL12:21 for L being Semilattice, F being upper filtered Subset of L holds F "/\" F = F; theorem :: WAYBEL12:22 for L being sup-Semilattice, I being lower directed Subset of L holds I "\/" I = I; theorem :: WAYBEL12:23 for L being upper-bounded Semilattice, V being Subset of L holds {x where x is Element of L : V "/\" {x} c= V} is non empty; theorem :: WAYBEL12:24 for L being antisymmetric transitive with_infima RelStr, V being Subset of L holds {x where x is Element of L : V "/\" {x} c= V} is filtered Subset of L; theorem :: WAYBEL12:25 for L being antisymmetric transitive 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; theorem :: WAYBEL12:26 for L being with_infima Poset, X being Subset of L st X is Open lower holds X is filtered; registration let L be with_infima Poset; cluster Open lower -> filtered for Subset of L; end; registration let L be continuous antisymmetric non empty reflexive RelStr; cluster lower -> Open for Subset of L; end; registration let L be continuous Semilattice, x be Element of L; cluster (downarrow x)` -> Open; end; theorem :: WAYBEL12:27 for L being Semilattice, C being non empty Subset of L st for x, y being Element of L st x in C & y in C holds x <= y or y <= x for Y being non empty finite Subset of C holds "/\"(Y,L) in Y; theorem :: WAYBEL12:28 for L being sup-Semilattice, C being non empty Subset of L st for x, y being Element of L st x in C & y in C holds x <= y or y <= x for Y being non empty finite Subset of C holds "\/"(Y,L) in Y; definition let L be Semilattice, F be Filter of L; mode GeneratorSet of F -> Subset of L means :: WAYBEL12:def 3 F = uparrow fininfs it; end; registration let L be Semilattice, F be Filter of L; cluster non empty for GeneratorSet of F; end; theorem :: WAYBEL12:29 for L being Semilattice, 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; theorem :: WAYBEL12:30 for L being Semilattice, F being Filter of L, 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; theorem :: WAYBEL12:31 for L being Semilattice, A being Subset of L for f, g being sequence of 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; theorem :: WAYBEL12:32 for L being Semilattice, F being Filter of L, G being GeneratorSet of F for f, g being sequence of 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; begin :: On the Baire Category Theorem :: Proposition 3.43.1 theorem :: WAYBEL12:33 for L being lower-bounded continuous LATTICE, V being Open upper Subset of L for F being Filter of L, 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 ex O being Open Filter of L st O c= V & v in O & F c= O; :: Corolarry 3.43.2 theorem :: WAYBEL12:34 for L being lower-bounded continuous LATTICE, V being Open upper 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 ex O being Open Filter of L st {v} "/\" N c= O & O c= V & v in O; :: Proposition 3.43.3 theorem :: WAYBEL12:35 for L being lower-bounded continuous LATTICE, V being Open upper Subset of L for N being non empty countable Subset of L, x, y being Element of L st V "/\" N c= V & y in V & not x in V ex p being irreducible Element of L st x <= p & not p in uparrow ({y} "/\" N); :: Corollary 3.43.4 theorem :: WAYBEL12:36 for L being lower-bounded continuous LATTICE, 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 for y being Element of L st not y <= x ex p being irreducible Element of L st x <= p & not p in uparrow ({y} "/\" N); :: Definition 3.43.5 definition let L be non empty RelStr, u be Element of L; attr u is dense means :: WAYBEL12:def 4 for v being Element of L st v <> Bottom L holds u "/\" v <> Bottom L; end; registration let L be upper-bounded Semilattice; cluster Top L -> dense; end; registration let L be upper-bounded Semilattice; cluster dense for Element of L; 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; definition let L be non empty RelStr, D be Subset of L; attr D is dense means :: WAYBEL12:def 5 for d being Element of L st d in D holds d is dense; end; theorem :: WAYBEL12:38 for L being upper-bounded Semilattice holds {Top L} is dense; registration let L be upper-bounded Semilattice; cluster non empty finite countable dense for Subset of L; end; :: Theorem 3.43.7 ::$N Baire Category Theorem for Continuous Lattices theorem :: WAYBEL12:39 for L being lower-bounded continuous LATTICE for D being non empty countable dense Subset of L, u being Element of L st u <> Bottom L ex p being irreducible Element of L st p <> Top L & not p in uparrow ({u} "/\" D); theorem :: 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; theorem :: 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; theorem :: 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; :: Theorem 3.43.8 theorem :: WAYBEL12:43 for T being non empty TopSpace st T is locally-compact for D being countable Subset-Family of T st D is non empty dense open for O being non empty Subset of T st O is open ex A being irreducible Subset of T st for V being Subset of T st V in D holds A /\ O meets V; 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 dense ex I being Subset of T st I = Intersect F & I is dense; end; :: Corolarry 3.43.10 theorem :: WAYBEL12:44 for T being non empty TopSpace st T is sober locally-compact holds T is Baire ;