Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### On the Baire Category Theorem

**by****Artur Kornilowicz**- Received February 5, 1997
- MML identifier: WAYBEL12

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, FUNCT_1, FINSET_1, BOOLE, FINSEQ_1, CARD_1, PRE_TOPC, SUBSET_1, SETFAM_1, TOPS_1, CARD_4, TARSKI, RELAT_1, RELAT_2, WAYBEL_0, YELLOW_0, ORDINAL2, LATTICE3, LATTICES, QUANTAL1, WAYBEL_6, WAYBEL_3, FINSUB_1, FILTER_0, FREEALG, ORDERS_2, REALSET1, YELLOW_1, TOPS_3, YELLOW_8, CANTOR_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, FINSUB_1, STRUCT_0, REALSET1, CARD_1, CARD_4, PRE_TOPC, ORDERS_1, TOPS_1, TOPS_2, TOPS_3, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8; constructors CARD_4, WAYBEL_3, WAYBEL_6, SETWISEO, YELLOW_4, REALSET1, TOPS_1, YELLOW_3, WAYBEL_4, TOPS_2, TOPS_3, NAT_1, CANTOR_1, YELLOW_8, WAYBEL_1, MEMBERED; clusters SUBSET_1, LATTICE3, WAYBEL_3, WAYBEL_6, WAYBEL_0, YELLOW_0, STRUCT_0, YELLOW_4, FINSET_1, CARD_1, YELLOW_6, YELLOW_1, WAYBEL_7, YELLOW_8, CANTOR_1, FINSUB_1, FINSEQ_1, RELSET_1, RLVECT_2, MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2; 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; definition cluster empty 1-sorted; end; definition let S be empty 1-sorted; cluster the carrier of S -> empty; end; definition let S be empty 1-sorted; cluster -> empty Subset of S; end; definition cluster finite -> countable set; end; definition cluster empty set; end; definition let S be 1-sorted; cluster empty Subset of S; end; definition cluster non empty finite set; end; definition let L be non empty RelStr; cluster non empty finite Subset of L; end; definition cluster NAT -> infinite; end; definition cluster infinite countable set; end; definition let S be 1-sorted; cluster empty Subset-Family of S; end; canceled; theorem :: WAYBEL12:2 for X, Y being set st Card X <=` Card Y & Y is countable holds X is countable; theorem :: WAYBEL12:3 for A being infinite countable set holds NAT,A are_equipotent; theorem :: WAYBEL12:4 for A being non empty countable set ex f being Function of NAT, A st rng f = A; theorem :: WAYBEL12:5 for S being 1-sorted, X, Y being Subset of S holds (X \/ Y)` = (X`) /\ Y`; theorem :: WAYBEL12:6 for S being 1-sorted, X, Y being Subset of S holds (X /\ Y)` = (X`) \/ Y`; theorem :: WAYBEL12:7 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:8 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:9 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:10 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:11 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:12 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:13 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:14 for L being lower-bounded with_infima antisymmetric RelStr for X being Subset of L holds X "/\" {Bottom L} c= {Bottom L}; theorem :: WAYBEL12:15 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:16 for L being upper-bounded with_suprema antisymmetric RelStr for X being Subset of L holds X "\/" {Top L} c= {Top L}; theorem :: WAYBEL12:17 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:18 for L being upper-bounded Semilattice, X being Subset of L holds {Top L} "/\" X = X; theorem :: WAYBEL12:19 for L being lower-bounded with_suprema Poset, X being Subset of L holds {Bottom L} "\/" X = X; theorem :: WAYBEL12:20 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:21 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:22 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:23 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:24 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:25 for L being Semilattice, F being upper filtered Subset of L holds F "/\" F = F; theorem :: WAYBEL12:26 for L being sup-Semilattice, I being lower directed Subset of L holds I "\/" I = I; theorem :: WAYBEL12:27 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:28 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:29 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:30 for L being with_infima Poset, X being Subset of L st X is Open lower holds X is filtered; definition let L be with_infima Poset; cluster Open lower -> filtered Subset of L; end; definition let L be continuous antisymmetric (non empty reflexive RelStr); cluster lower -> Open Subset of L; end; definition let L be continuous Semilattice, x be Element of L; cluster (downarrow x)` -> Open; end; theorem :: WAYBEL12:31 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:32 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; definition let L be Semilattice, F be Filter of L; cluster non empty GeneratorSet of F; end; theorem :: WAYBEL12:33 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:34 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:35 for L being Semilattice, 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 Nat: m <= n},L) holds A is_coarser_than rng g; theorem :: WAYBEL12:36 for L being Semilattice, F being Filter of L, 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 Nat: m <= n},L) holds rng g is GeneratorSet of F; begin :: On the Baire Category Theorem :: Proposition 3.43.1 theorem :: WAYBEL12:37 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:38 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:39 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:40 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; definition let L be upper-bounded Semilattice; cluster Top L -> dense; end; definition let L be upper-bounded Semilattice; cluster dense Element of L; end; theorem :: WAYBEL12:41 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:42 for L being upper-bounded Semilattice holds {Top L} is dense; definition let L be upper-bounded Semilattice; cluster non empty finite countable dense Subset of L; end; :: Theorem 3.43.7 theorem :: WAYBEL12:43 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:44 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:45 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:46 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:47 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:48 for T being non empty TopSpace st T is sober locally-compact holds T is Baire;

Back to top