:: 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 b₁ being Subset of L st b₁ is Open & b₁ is lower holds
b₁ 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 b₁ being Subset of L st b₁ is lower holds
b₁ 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 b₁ being Subset of L st F = uparrow (fininfs b₁)

proof end;

end;

:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :
for L being Semilattice
for F being Filter of L
for b₃ being Subset of L holds
( b₃ is GeneratorSet of F iff F = uparrow (fininfs b₃) );

registration

let L be Semilattice;
let F be Filter of L;

cluster non empty for GeneratorSet of F;

existence
not for b₁ being GeneratorSet of F holds b₁ 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 b₁ being Element of L st b₁ 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 b₁ being Subset of L st
( not b₁ is empty & b₁ is finite & b₁ is countable & b₁ is dense )

proof end;

end;

:: Theorem 3.43.7
:: 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;