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


Lm1: for L being non empty RelStr
for f being sequence of 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 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 ) ;
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;
attr F is dense means :: WAYBEL12:def 2
 for X being Subset of T st X in F holds
X is dense ;
end;

:: deftheorem 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 end;

theorem :: WAYBEL12:2
for A being denumerable set holds NAT ,A are_equipotent
proof 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 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 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 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 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 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 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 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 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 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 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 end;

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

theorem :: WAYBEL12:15
for L being lower-bounded with_suprema Poset
for X being Subset of L holds {(Bottom L)} "\/" X = X
proof 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 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 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 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 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 end;

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

theorem :: WAYBEL12:22
for L being sup-Semilattice
for I being directed lower Subset of L holds I "\/" I = I
proof 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 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 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 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 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 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 end;
end;

registration
let L be continuous Semilattice;
let x be Element of L;
cluster (downarrow x) ` -> Open ;
coherence
(downarrow x) ` is Open
proof 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 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 end;

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

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

Lm4: for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
proof 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 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 end;

theorem Th31: :: WAYBEL12:31
for L being Semilattice
for 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
proof 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 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
proof end;

:: 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 & 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 end;

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

:: 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 & 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 end;

:: 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 & 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 end;

:: Definition 3.43.5
definition
let L be non empty RelStr ;
let 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;

:: deftheorem 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 by WAYBEL_1:4;
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 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 end;

definition
let L be non empty RelStr ;
let D be Subset of L;
attr D 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 by TARSKI:def 1;

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 end;
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 & not p in uparrow ({u} "/\" D) )
proof 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 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 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 end;

:: 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 & 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 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 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 ) );

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