:: On the Baire Category Theorem
:: by Artur Korni{\l}owicz
::
:: Received February 5, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


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
proofend;

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 )
proofend;
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 &amp; Y is countable holds
X is countable
proofend;

theorem :: WAYBEL12:2
for A being denumerable set holds NAT ,A are_equipotent
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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)}
proofend;

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)}
proofend;

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)}
proofend;

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)}
proofend;

theorem Th14: :: WAYBEL12:14
for L being upper-bounded Semilattice
for X being Subset of L holds {(Top L)} "/\" X = X
proofend;

theorem :: WAYBEL12:15
for L being lower-bounded with_suprema Poset
for X being Subset of L holds {(Bottom L)} "\/" X = X
proofend;

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 &amp; A is_coarser_than B )
proofend;

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
proofend;

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
proofend;

theorem Th19: :: WAYBEL12:19
for L being non empty RelStr
for V, S, T being Subset of L st S is_coarser_than T &amp; V is upper &amp; T c= V holds
S c= V
proofend;

theorem :: WAYBEL12:20
for L being non empty RelStr
for V, S, T being Subset of L st S is_finer_than T &amp; V is lower &amp; T c= V holds
S c= V
proofend;

theorem Th21: :: WAYBEL12:21
for L being Semilattice
for F being filtered upper Subset of L holds F "/\" F = F
proofend;

theorem :: WAYBEL12:22
for L being sup-Semilattice
for I being directed lower Subset of L holds I "\/" I = I
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

theorem Th26: :: WAYBEL12:26
for L being with_infima Poset
for X being Subset of L st X is Open &amp; X is lower holds
X is filtered
proofend;

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 &amp; 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
proofend;
end;

registration
let L be continuous Semilattice;
let x be Element of L;
cluster(downarrow x) `  ->  Open ;
coherence
 (downarrow x) ` is Open
proofend;
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 &amp; y in C &amp; not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "/\" (Y,L) in Y
proofend;

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 &amp; y in C &amp; not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "\/" (Y,L) in Y
proofend;

Lm3:  for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
proofend;

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)
proofend;
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
proofend;
end;

Lm4:  for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
proofend;

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
proofend;

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 &amp; A is_coarser_than F holds
A is GeneratorSet of F
proofend;

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 &amp; ( 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
proofend;

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 &amp; ( 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
proofend;

begin

:: Proposition 3.43.1
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 &amp; v in V &amp; ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V &amp; v in O &amp; F c= O )
proofend;

:: Corolarry 3.43.2
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 &amp; v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O &amp; O c= V &amp; v in O )
proofend;

:: Proposition 3.43.3
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 &amp; y in V &amp; not x in V holds
ex p being irreducible Element of L st
( x <= p &amp; not p in uparrow ({y} "/\" N) )
proofend;

:: Corollary 3.43.4
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 &amp; 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 &amp; not p in uparrow ({y} "/\" N) )
proofend;

:: Definition 3.43.5
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
proofend;
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
proofend;
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
proofend;

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
proofend;

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 &amp; b1 is finite &amp; b1 is countable &amp; b1 is dense )
proofend;
end;

:: Theorem 3.43.7
:: [WP: ] Baire_Category_Theorem_for_Continuous_Lattices
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 &amp; not p in uparrow ({u} "/\" D) )
proofend;

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 &amp; B ` is irreducible holds
A is irreducible
proofend;

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 &amp; A <> Top (InclPoset the topology of T) holds
( A is irreducible iff B ` is irreducible )
proofend;

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 )
proofend;

:: Theorem 3.43.8
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 &amp; D is dense &amp; 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
proofend;

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 &amp; ( for S being Subset of T st S in F holds
( S is open &amp; S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F &amp; I is dense );
compatibility
 ( T is Baire iff for F being Subset-Family of T st F is countable &amp; ( for S being Subset of T st S in F holds
( S is open &amp; S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F &amp; I is dense ) )
proofend;
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 &amp; ( for S being Subset of T st S in F holds
( S is open &amp; S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F &amp; I is dense ) );

:: Corolarry 3.43.10
theorem :: WAYBEL12:44
for T being non empty TopSpace st T is sober &amp; T is locally-compact holds
T is Baire
proofend;