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;