:: On the Baire Category Theorem
:: by Artur Korni{\l}owicz
::
:: Received February 5, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ORDERS_2, FUNCT_1, NUMBERS, STRUCT_0, SUBSET_1,
XXREAL_0, FINSET_1, TARSKI, CARD_1, FINSEQ_1, PRE_TOPC, RCOMP_1,
SETFAM_1, TOPS_1, CARD_3, ORDINAL1, RELAT_2, WAYBEL_0, YELLOW_0,
ORDINAL2, LATTICE3, LATTICES, EQREL_1, WAYBEL_6, WAYBEL_3, FINSUB_1,
CARD_FIL, MSAFREE, RELAT_1, ARYTM_3, YELLOW_8, ORDERS_1, ZFMISC_1,
XXREAL_2, YELLOW_1, TOPS_3, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, NAT_1, SETFAM_1, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1,
FINSUB_1, DOMAIN_1, XXREAL_0, FUNCT_2, STRUCT_0, CARD_3, PRE_TOPC,
ORDERS_2, TOPS_1, TOPS_2, TOPS_3, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0,
YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8;
constructors SETFAM_1, DOMAIN_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, TOPS_1,
TOPS_2, TOPS_3, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4,
WAYBEL_6, YELLOW_8, RELSET_1, FINSEQ_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XREAL_0,
CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, PRE_TOPC, WAYBEL_0,
YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_3, YELLOW_6, WAYBEL_6, WAYBEL_7,
YELLOW_8, SETWISEO, CARD_3, TOPS_1, RELAT_1;
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;
theorem :: WAYBEL12:1
for X, Y being set st card X c= card Y & Y is countable holds X is countable;
theorem :: WAYBEL12:2
for A being denumerable set holds NAT,A are_equipotent;
theorem :: WAYBEL12:3
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:4
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:5
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:6
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:7
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:8
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:9
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:10
for L being lower-bounded with_infima antisymmetric RelStr for X
being Subset of L holds X "/\" {Bottom L} c= {Bottom L};
theorem :: WAYBEL12:11
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:12
for L being upper-bounded with_suprema antisymmetric RelStr for
X being Subset of L holds X "\/" {Top L} c= {Top L};
theorem :: WAYBEL12:13
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:14
for L being upper-bounded Semilattice, X being Subset of L holds
{Top L} "/\" X = X;
theorem :: WAYBEL12:15
for L being lower-bounded with_suprema Poset, X being Subset of L
holds {Bottom L} "\/" X = X;
theorem :: WAYBEL12:16
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:17
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:18
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:19
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:20
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:21
for L being Semilattice, F being upper filtered Subset of L
holds F "/\" F = F;
theorem :: WAYBEL12:22
for L being sup-Semilattice, I being lower directed Subset of L holds
I "\/" I = I;
theorem :: WAYBEL12:23
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:24
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:25
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:26
for L being with_infima Poset, X being Subset of L st X is Open
lower holds X is filtered;
registration
let L be with_infima Poset;
cluster Open lower -> filtered for Subset of L;
end;
registration
let L be continuous antisymmetric non empty reflexive RelStr;
cluster lower -> Open for Subset of L;
end;
registration
let L be continuous Semilattice, x be Element of L;
cluster (downarrow x)` -> Open;
end;
theorem :: WAYBEL12:27
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:28
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;
registration
let L be Semilattice, F be Filter of L;
cluster non empty for GeneratorSet of F;
end;
theorem :: WAYBEL12:29
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:30
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:31
for L being Semilattice, 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;
theorem :: WAYBEL12:32
for L being Semilattice, F being Filter of L, 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;
begin :: On the Baire Category Theorem
:: Proposition 3.43.1
theorem :: WAYBEL12:33
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:34
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:35
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:36
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;
registration
let L be upper-bounded Semilattice;
cluster Top L -> dense;
end;
registration
let L be upper-bounded Semilattice;
cluster dense for Element of L;
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;
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:38
for L being upper-bounded Semilattice holds {Top L} is dense;
registration
let L be upper-bounded Semilattice;
cluster non empty finite countable dense for Subset of L;
end;
:: Theorem 3.43.7
::$N Baire Category Theorem for Continuous Lattices
theorem :: WAYBEL12:39
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: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;
theorem :: 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;
theorem :: 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;
:: Theorem 3.43.8
theorem :: WAYBEL12:43
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:44
for T being non empty TopSpace st T is sober locally-compact holds T is Baire
;