:: On the {B}orel Families of Subsets of Topological Spaces
:: by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005-2026 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 STRUCT_0, SETFAM_1, ZFMISC_1, CARD_3, TARSKI, NUMBERS, FUNCT_1,
RELAT_1, CARD_1, ORDINAL1, SUBSET_1, XBOOLE_0, PRE_TOPC, TOPGEN_1,
FINSET_1, WAYBEL23, RCOMP_1, RLVECT_3, TOPS_1, CONNSP_1, PCOMPS_1,
NATTRA_1, PROB_1, MEASURE1, MCART_1, TOPMETR, CONNSP_2, WAYBEL30,
OPENLATT, EQREL_1, NAT_1, TOPGEN_4;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, FUNCT_1,
CARD_1, ORDINAL1, NUMBERS, CARD_3, MCART_1, WELLORD2, FINSET_1, SETFAM_1,
DOMAIN_1, CONNSP_2, ZFMISC_1, STRUCT_0, OPENLATT, MEASURE1, PRE_TOPC,
TOPS_1, TOPS_2, CONNSP_1, TDLAT_3, WAYBEL23, PROB_1, TOPMETR, CANTOR_1,
ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1;
constructors MEASURE1, TOPS_1, CONNSP_1, COMPTS_1, TDLAT_3, TOPMETR, OPENLATT,
WAYBEL23, TOPGEN_2, ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1, XTUPLE_0,
XFAMILY;
registrations SUBSET_1, RELSET_1, FINSET_1, NUMBERS, CARD_1, MEASURE1,
STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TOPMETR, TOPREAL6, TOPGEN_2,
TOPGEN_1, CARD_3, COMPTS_1, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, STRUCT_0, OPENLATT;
expansions TARSKI, XBOOLE_0, CARD_3, MEASURE1;
theorems TARSKI, SETFAM_1, FUNCT_1, FUNCT_2, ZFMISC_1, PRE_TOPC, TOPS_1,
XBOOLE_1, SUBSET_1, YELLOW_8, WAYBEL23, TOPMETR, NUMBERS, CONNSP_1,
CONNSP_2, CARD_4, CARD_1, PCOMPS_1, XBOOLE_0, TOPGEN_1, TOPS_2, MEASURE1,
WAYBEL12, MCART_1, TSP_1, TOPGEN_2, TOPGEN_3, PROB_1, CARD_2, TOPS_3,
NAT_1, CARD_3;
schemes FUNCT_1, TREES_2, BORSUK_2, SUBSET_1, XFAMILY;
begin :: Preliminaries
definition
let T be 1-sorted;
func TotFam T -> Subset-Family of T equals
bool the carrier of T;
coherence by ZFMISC_1:def 1;
end;
theorem Th1:
for T being set, F being Subset-Family of T holds F is countable
iff COMPLEMENT F is countable
proof
let T be set, F be Subset-Family of T;
F, COMPLEMENT F are_equipotent by YELLOW_8:3;
hence thesis by YELLOW_8:4;
end;
registration
cluster RAT -> countable;
coherence by TOPGEN_3:17;
end;
Lm1: for X being set holds X is countable iff ex f being Function st dom f =
RAT & X c= rng f
by CARD_1:12,TOPGEN_3:17;
scheme FraenCoun11 { P[set] } :
{ {n} where n is Element of RAT : P[n] } is countable
proof
deffunc g(object) = { $1 };
consider f being Function such that
A1: dom f = RAT & for x being object st x in RAT holds f.x = g(x) from
FUNCT_1:sch 3;
{ {n} where n is Element of RAT : P[n] } c= rng f
proof
let x be object;
assume x in { {n} where n is Element of RAT : P[n] };
then consider n be Element of RAT such that
A2: x = {n} and
P[n];
f.n = x by A1,A2;
hence thesis by A1,FUNCT_1:def 3;
end;
hence thesis by A1,Lm1;
end;
theorem
for T being non empty TopSpace, A being Subset of T holds Der A = { x
where x is Point of T : x in Cl (A \ {x}) }
proof
let T be non empty TopSpace, A be Subset of T;
thus Der A c= { x where x is Point of T : x in Cl (A \ {x}) }
proof
let x be object;
assume x in Der A;
then x is_an_accumulation_point_of A by TOPGEN_1:def 3;
then x in Cl (A \ {x}) by TOPGEN_1:def 2;
hence thesis;
end;
let y be object;
assume y in { x where x is Point of T : x in Cl (A \ {x}) };
then consider z being Point of T such that
A1: z = y and
A2: z in Cl (A \ {z});
z is_an_accumulation_point_of A by A2,TOPGEN_1:def 2;
hence thesis by A1,TOPGEN_1:def 3;
end;
registration
cluster finite -> second-countable for TopStruct;
coherence
proof
let T be TopStruct;
assume T is finite;
then reconsider T9 = T as finite TopStruct;
weight T9 is finite by TOPGEN_2:def 4;
then weight T9 c= omega;
hence thesis by WAYBEL23:def 6;
end;
end;
registration
cluster REAL -> non countable;
coherence
by TOPGEN_3:30,TOPGEN_3:def 4;
end;
registration
cluster non countable -> non finite for set;
coherence;
cluster non finite -> non trivial for set;
coherence;
cluster non countable non empty for set;
existence
proof
take REAL;
thus thesis;
end;
end;
reserve T for non empty TopSpace,
A, B for Subset of T,
F, G for Subset-Family of T;
theorem
A is closed iff Der A c= A
proof
hereby
assume A is closed;
then
A1: A = Cl A by PRE_TOPC:22;
Cl A = A \/ Der A by TOPGEN_1:29;
hence Der A c= A by A1,XBOOLE_1:7;
end;
assume
A2: Der A c= A;
Cl A = A \/ Der A by TOPGEN_1:29
.= A by A2,XBOOLE_1:12;
hence thesis;
end;
theorem Th4:
for T being non empty TopStruct, B being Basis of T, V being
Subset of T st V is open & V <> {} ex W being Subset of T st W in B & W c= V &
W <> {}
proof
let T be non empty TopStruct, B be Basis of T, V be Subset of T;
assume that
A1: V is open and
A2: V <> {};
consider x being object such that
A3: x in V by A2,XBOOLE_0:def 1;
V = union { G where G is Subset of T : G in B & G c= V } by A1,YELLOW_8:9;
then consider Y being set such that
A4: x in Y and
A5: Y in { G where G is Subset of T : G in B & G c= V } by A3,TARSKI:def 4;
ex Z being Subset of T st Z = Y & Z in B & Z c= V by A5;
hence thesis by A4;
end;
begin :: Regular Formalization: Separable Spaces
:: 1.3.7. Theorem
theorem Th5:
density T c= weight T
proof
defpred P[set] means $1 <> {};
deffunc F(set) = the Element of $1;
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= B and
A1: card B1 = weight T by TOPGEN_2:18;
set A = { F(BB) where BB is Element of bool the carrier of T : BB in B1 & P[
BB] };
A c= the carrier of T
proof
let x be object;
assume x in A;
then consider B2 being Subset of T such that
A2: x = the Element of B2 and
B2 in B1 and
A3: B2 <> {};
x in B2 by A2,A3;
hence thesis;
end;
then reconsider A as Subset of T;
for Q being Subset of T st Q <> {} & Q is open holds A meets Q
proof
let Q be Subset of T;
assume Q <> {} & Q is open;
then consider W being Subset of T such that
A4: W in B1 and
A5: W c= Q and
A6: W <> {} by Th4;
the Element of W in A & the Element of W in W by A4,A6;
hence thesis by A5,XBOOLE_0:3;
end;
then A is dense by TOPS_1:45;
then
A7: density T c= card A by TOPGEN_1:def 12;
card { F(w) where w is Element of bool the carrier of T : w in B1 & P[w
] } c= card B1 from BORSUK_2:sch 1;
hence thesis by A1,A7;
end;
theorem
T is separable iff ex A being Subset of T st A is dense countable
proof
hereby
consider A being Subset of T such that
A1: A is dense and
A2: density T = card A by TOPGEN_1:def 12;
assume T is separable;
then density T c= omega by TOPGEN_1:def 13;
then A is countable by A2;
hence ex A being Subset of T st A is dense countable by A1;
end;
given A being Subset of T such that
A3: A is dense countable;
density T c= card A & card A c= omega by A3,TOPGEN_1:def 12;
then density T c= omega;
hence thesis by TOPGEN_1:def 13;
end;
:: 1.3.8. Corollary
theorem Th7:
T is second-countable implies T is separable
proof
assume T is second-countable;
then
A1: weight T c= omega by WAYBEL23:def 6;
density T c= weight T by Th5;
then density T c= omega by A1;
hence thesis by TOPGEN_1:def 13;
end;
registration
cluster second-countable -> separable for non empty TopSpace;
coherence by Th7;
end;
:: Exercises
theorem :: Exercise 1.3.A.
for T being non empty TopSpace, A, B being Subset of T st A, B
are_separated holds Fr (A \/ B) = Fr A \/ Fr B
proof
let T be non empty TopSpace, A, B be Subset of T;
A1: Fr A \/ Fr B = Fr (A \/ B) \/ Fr (A /\ B) \/ (Fr A /\ Fr B) & Fr {}T =
{} by TOPS_1:36;
assume
A2: A, B are_separated;
then
A3: A misses Cl B by CONNSP_1:def 1;
A misses B by A2,CONNSP_1:1;
then
A4: A /\ B = {};
A5: Cl A misses B by A2,CONNSP_1:def 1;
A6: Fr A \/ Fr B c= Fr (A \/ B)
proof
let x be object;
assume
A7: x in Fr A \/ Fr B;
per cases by A4,A1,A7,XBOOLE_0:def 3;
suppose
x in Fr (A \/ B);
hence thesis;
end;
suppose
A8: x in Fr A /\ Fr B;
then x in Fr B by XBOOLE_0:def 4;
then x in Cl B /\ Cl B` by TOPS_1:def 2;
then x in Cl B by XBOOLE_0:def 4;
then not x in A by A3,XBOOLE_0:3;
then
A9: x in A` by A7,XBOOLE_0:def 5;
x in Fr A by A8,XBOOLE_0:def 4;
then x in Cl A /\ Cl A` by TOPS_1:def 2;
then
A10: x in Cl A by XBOOLE_0:def 4;
then x in Cl A \/ Cl B by XBOOLE_0:def 3;
then
A11: x in Cl (A \/ B) by PRE_TOPC:20;
not x in B by A5,A10,XBOOLE_0:3;
then x in B` by A7,XBOOLE_0:def 5;
then x in A` /\ B` by A9,XBOOLE_0:def 4;
then
A12: x in (A \/ B)` by XBOOLE_1:53;
(A \/ B)` c= Cl (A \/ B)` by PRE_TOPC:18;
then x in Cl (A \/ B) /\ Cl (A \/ B)` by A11,A12,XBOOLE_0:def 4;
hence thesis by TOPS_1:def 2;
end;
end;
Fr (A \/ B) c= Fr A \/ Fr B by TOPS_1:33;
hence thesis by A6;
end;
:: Exercise 1.3.B.
theorem :: Ex. 1.3.B. a)
F is locally_finite implies Fr union F c= union Fr F
proof
assume F is locally_finite;
then
A1: Cl union F = union clf F by PCOMPS_1:20;
let x be object;
assume x in Fr union F;
then
A2: x in Cl union F /\ Cl (union F)` by TOPS_1:def 2;
then
A3: x in Cl (union F)` by XBOOLE_0:def 4;
x in Cl union F by A2,XBOOLE_0:def 4;
then consider A being set such that
A4: x in A and
A5: A in clf F by A1,TARSKI:def 4;
consider B being Subset of T such that
A6: A = Cl B and
A7: B in F by A5,PCOMPS_1:def 2;
B c= union F by A7,ZFMISC_1:74;
then (union F)` c= B` by SUBSET_1:12;
then Cl (union F)` c= Cl B` by PRE_TOPC:19;
then x in Cl B /\ Cl B` by A4,A6,A3,XBOOLE_0:def 4;
then
A8: x in Fr B by TOPS_1:def 2;
Fr B in Fr F by A7,TOPGEN_1:def 1;
hence thesis by A8,TARSKI:def 4;
end;
theorem Th10: :: also for empty TopSpaces
for T being discrete non empty TopSpace holds T is separable iff
card [#]T c= omega
proof
let T be discrete non empty TopSpace;
hereby
assume T is separable;
then
A1: density T c= omega by TOPGEN_1:def 13;
ex A being Subset of T st A is dense & density T = card A by
TOPGEN_1:def 12;
hence card [#]T c= omega by A1,TOPS_3:19;
end;
assume card [#]T c= omega;
then T is countable by TOPGEN_1:2;
hence thesis;
end;
theorem
for T being discrete non empty TopSpace holds T is separable iff T is
countable
proof
let T be discrete non empty TopSpace;
T is separable iff card [#]T c= omega by Th10;
hence thesis by TOPGEN_1:2;
end;
begin :: Families of Subsets Closed for Countable Unions and Complement
definition
let T, F;
attr F is all-open-containing means
:Def2:
for A being Subset of T st A is open holds A in F;
end;
definition
let T, F;
attr F is all-closed-containing means
:Def3:
for A being Subset of T st A is closed holds A in F;
end;
definition
let T be set, F be Subset-Family of T;
attr F is closed_for_countable_unions means
:Def4:
for G being countable Subset-Family of T st G c= F holds union G in F;
end;
Lm2: for T being set, F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
proof
let T be set, F be Subset-Family of T;
assume
A1: F is SigmaField of T;
let G be countable Subset-Family of T;
assume
A2: G c= F;
per cases;
suppose
G is empty;
hence thesis by A1,PROB_1:4,ZFMISC_1:2;
end;
suppose
G is non empty;
hence thesis by A1,A2,MEASURE1:def 5;
end;
end;
registration
let T be set;
cluster -> closed_for_countable_unions for SigmaField of T;
coherence by Lm2;
end;
theorem
for T being set, F being Subset-Family of T st F is
closed_for_countable_unions holds {} in F
proof
let T be set, F be Subset-Family of T;
reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;
A1: E c= F;
assume F is closed_for_countable_unions;
hence thesis by A1,ZFMISC_1:2;
end;
registration
let T be set;
cluster closed_for_countable_unions -> non empty for Subset-Family of T;
coherence;
end;
theorem Th13:
for T being set, F being Subset-Family of T holds F is
SigmaField of T iff F is compl-closed closed_for_countable_unions
proof
let T be set, F be Subset-Family of T;
thus F is SigmaField of T implies F is compl-closed
closed_for_countable_unions;
assume
A1: F is compl-closed closed_for_countable_unions;
F is sigma-additive
by A1;
then reconsider
F as non empty compl-closed sigma-additive Subset-Family of T by A1;
F is SigmaField of T;
hence thesis;
end;
definition
let T be set, F be Subset-Family of T;
attr F is closed_for_countable_meets means
:Def5:
for G being countable Subset-Family of T st G c= F holds meet G in F;
end;
theorem Th14:
for F being Subset-Family of T holds F is all-closed-containing
compl-closed iff F is all-open-containing compl-closed
proof
let F be Subset-Family of T;
hereby
assume
A1: F is all-closed-containing compl-closed;
for A being Subset of T st A is open holds A in F
proof
let A be Subset of T;
assume A is open;
then A` in F by A1;
then A`` in F by A1;
hence thesis;
end;
hence F is all-open-containing compl-closed by A1;
end;
assume
A2: F is all-open-containing compl-closed;
for A being Subset of T st A is closed holds A in F
proof
let A be Subset of T;
assume A is closed;
then A` in F by A2;
then A`` in F by A2;
hence thesis;
end;
hence thesis by A2;
end;
theorem
for T being set, F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
proof
let T be set, F be Subset-Family of T;
assume
A1: F is compl-closed;
thus F c= COMPLEMENT F
proof
let x be object;
assume
A2: x in F;
then reconsider x9 = x as Subset of T;
x9` in F by A1,A2;
hence thesis by SETFAM_1:def 7;
end;
let x be object;
assume
A3: x in COMPLEMENT F;
then reconsider x9 = x as Subset of T;
x9` in F by A3,SETFAM_1:def 7;
then x9`` in F by A1;
hence thesis;
end;
theorem Th16:
for T being set, F, G being Subset-Family of T st F c= G & G is
compl-closed holds COMPLEMENT F c= G
proof
let T be set, F, G be Subset-Family of T;
assume
A1: F c= G & G is compl-closed;
let x be object;
assume
A2: x in COMPLEMENT F;
then reconsider x9 = x as Subset of T;
x9` in F by A2,SETFAM_1:def 7;
then x9`` in G by A1;
hence thesis;
end;
theorem Th17:
for T being set, F being Subset-Family of T holds F is
closed_for_countable_meets compl-closed iff F is closed_for_countable_unions
compl-closed
proof
let T be set, F be Subset-Family of T;
hereby
assume
A1: F is closed_for_countable_meets compl-closed;
for G being countable Subset-Family of T st G c= F holds union G in F
proof
let G be countable Subset-Family of T;
assume
A2: G c= F;
per cases;
suppose
G = {};
hence thesis by A1,A2,SETFAM_1:1,ZFMISC_1:2;
end;
suppose
G <> {};
then reconsider G9 = G as non empty Subset-Family of T;
COMPLEMENT G9 c= F & COMPLEMENT G9 is countable by A1,A2,Th1,Th16;
then
A3: meet COMPLEMENT G9 in F by A1;
(meet COMPLEMENT G9)` = (union G9)`` by TOPS_2:6
.= union G9;
hence thesis by A1,A3;
end;
end;
hence F is closed_for_countable_unions compl-closed by A1;
end;
assume
A4: F is closed_for_countable_unions compl-closed;
for G being countable Subset-Family of T st G c= F holds meet G in F
proof
let G be countable Subset-Family of T;
assume
A5: G c= F;
per cases;
suppose
G = {};
hence thesis by A4,A5,SETFAM_1:1,ZFMISC_1:2;
end;
suppose
G <> {};
then reconsider G9 = G as non empty Subset-Family of T;
COMPLEMENT G9 c= F & COMPLEMENT G9 is countable by A4,A5,Th1,Th16;
then
A6: union COMPLEMENT G9 in F by A4;
(union COMPLEMENT G9)` = (meet G9)`` by TOPS_2:7
.= meet G9;
hence thesis by A4,A6;
end;
end;
hence thesis by A4;
end;
registration
let T;
cluster all-open-containing compl-closed closed_for_countable_unions ->
all-closed-containing closed_for_countable_meets for Subset-Family of T;
coherence by Th14,Th17;
cluster all-closed-containing compl-closed closed_for_countable_meets ->
all-open-containing closed_for_countable_unions for Subset-Family of T;
coherence by Th14,Th17;
end;
begin :: On the Families of Subsets
registration
let T be set;
let F be countable Subset-Family of T;
cluster COMPLEMENT F -> countable;
coherence by Th1;
end;
registration
let T be TopSpace;
cluster empty -> open closed for Subset-Family of T;
coherence
proof
let F be Subset-Family of T;
assume F is empty; then
( for P being Subset of T holds P in F implies P is open)& for P being
Subset of T holds P in F implies P is closed;
hence thesis by TOPS_2:def 1,def 2;
end;
end;
registration
let T be TopSpace;
cluster countable open closed for Subset-Family of T;
existence
proof
{}bool the carrier of T is open;
hence thesis;
end;
end;
theorem Th18:
for T being set holds {} is empty Subset-Family of T
proof
let T be set;
{}bool T = {};
hence thesis;
end;
registration
cluster empty -> countable for set;
coherence;
end;
begin :: Collective Properties of Families
theorem Th19:
F = { A } implies (A is open iff F is open)
proof
assume
A1: F = { A };
hereby
assume A is open;
then for A being Subset of T st A in F holds A is open by A1,TARSKI:def 1;
hence F is open by TOPS_2:def 1;
end;
assume
A2: F is open;
A in F by A1,TARSKI:def 1;
hence thesis by A2,TOPS_2:def 1;
end;
theorem Th20:
F = { A } implies (A is closed iff F is closed)
proof
assume
A1: F = { A };
hereby
assume A is closed;
then for A being Subset of T st A in F holds A is closed by A1,TARSKI:def 1
;
hence F is closed by TOPS_2:def 2;
end;
assume
A2: F is closed;
A in F by A1,TARSKI:def 1;
hence thesis by A2,TOPS_2:def 2;
end;
definition
let T be set, F, G be Subset-Family of T;
redefine func INTERSECTION (F,G) -> Subset-Family of T; :: redefines INTERSECTION (SETFAM_1, definition)
coherence
proof
INTERSECTION (F,G) c= bool T
proof
let x be object;
assume x in INTERSECTION (F,G);
then consider X, Y being set such that
A1: X in F and
Y in G and
A2: x = X /\ Y by SETFAM_1:def 5;
X /\ Y c= X by XBOOLE_1:17;
then x is Subset of T by A1,A2,XBOOLE_1:1;
hence thesis;
end;
hence thesis;
end;
redefine func UNION (F,G) -> Subset-Family of T; :: redefines UNION (SETFAM_1, definition)
coherence
proof
UNION (F,G) c= bool T
proof
let x be object;
assume x in UNION (F,G);
then consider X, Y being set such that
A3: X in F & Y in G and
A4: x = X \/ Y by SETFAM_1:def 4;
X \/ Y c= T by A3,XBOOLE_1:8;
hence thesis by A4;
end;
hence thesis;
end;
end;
theorem Th21:
F is closed & G is closed implies INTERSECTION (F,G) is closed
proof
assume
A1: F is closed & G is closed;
for A being Subset of T st A in INTERSECTION (F,G) holds A is closed
proof
let A be Subset of T;
assume A in INTERSECTION (F,G);
then consider X, Y being set such that
A2: X in F & Y in G and
A3: A = X /\ Y by SETFAM_1:def 5;
reconsider X, Y as Subset of T by A2;
X is closed & Y is closed by A1,A2,TOPS_2:def 2;
hence thesis by A3;
end;
hence thesis by TOPS_2:def 2;
end;
theorem Th22:
F is closed & G is closed implies UNION (F,G) is closed
proof
assume
A1: F is closed & G is closed;
for A being Subset of T st A in UNION (F,G) holds A is closed
proof
let A be Subset of T;
assume A in UNION (F,G);
then consider X, Y being set such that
A2: X in F & Y in G and
A3: A = X \/ Y by SETFAM_1:def 4;
reconsider X, Y as Subset of T by A2;
X is closed & Y is closed by A1,A2,TOPS_2:def 2;
hence thesis by A3;
end;
hence thesis by TOPS_2:def 2;
end;
theorem Th23:
F is open & G is open implies INTERSECTION (F,G) is open
proof
assume
A1: F is open & G is open;
for A being Subset of T st A in INTERSECTION (F,G) holds A is open
proof
let A be Subset of T;
assume A in INTERSECTION (F,G);
then consider X, Y being set such that
A2: X in F & Y in G and
A3: A = X /\ Y by SETFAM_1:def 5;
reconsider X, Y as Subset of T by A2;
X is open & Y is open by A1,A2,TOPS_2:def 1;
hence thesis by A3;
end;
hence thesis by TOPS_2:def 1;
end;
theorem Th24:
F is open & G is open implies UNION (F,G) is open
proof
assume
A1: F is open & G is open;
for A being Subset of T st A in UNION (F,G) holds A is open
proof
let A be Subset of T;
assume A in UNION (F,G);
then consider X, Y being set such that
A2: X in F & Y in G and
A3: A = X \/ Y by SETFAM_1:def 4;
reconsider X, Y as Subset of T by A2;
X is open & Y is open by A1,A2,TOPS_2:def 1;
hence thesis by A3;
end;
hence thesis by TOPS_2:def 1;
end;
theorem Th25:
for T being set, F, G being Subset-Family of T holds card
INTERSECTION (F,G) c= card [:F,G:]
proof
deffunc F(set) = $1`1 /\ $1`2;
let T be set, F, G be Subset-Family of T;
set XX = [:F,G:];
set IN = { F(X) where X is Element of [:bool T, bool T:] : X in XX };
set A = [:bool T, bool T:];
set AL = F, BL = G;
set C = INTERSECTION(AL,BL);
A1: IN c= C
proof
let a be object;
assume a in IN;
then consider X being Element of [:bool T, bool T:] such that
A2: a = F(X) and
A3: X in XX;
X`1 in F & X`2 in G by A3,MCART_1:10;
hence thesis by A2,SETFAM_1:def 5;
end;
A4: C c= IN
proof
let a be object;
assume a in C;
then consider X,Y be set such that
A5: X in AL & Y in BL and
A6: a = X /\ Y by SETFAM_1:def 5;
reconsider X,Y as Subset of T by A5;
set XY = [X,Y];
A7: XY`1 = X & XY`2 = Y;
XY in XX by A5,ZFMISC_1:87;
hence thesis by A6,A7;
end;
card { F(w) where w is Element of A : w in XX } c= card XX from TREES_2:
sch 2;
hence thesis by A1,A4,XBOOLE_0:def 10;
end;
theorem Th26:
for T being set, F, G being Subset-Family of T holds card UNION
(F,G) c= card [:F,G:]
proof
deffunc F(set) = $1`1 \/ $1`2;
let T be set, F, G be Subset-Family of T;
set XX = [:F,G:];
set IN = { F(X) where X is Element of [:bool T, bool T:] : X in XX };
set A = [:bool T, bool T:];
set AL = F, BL = G;
set C = UNION(AL,BL);
A1: IN = C
proof
thus IN c= C
proof
let a be object;
assume a in IN;
then consider X being Element of [:bool T, bool T:] such that
A2: a = F(X) and
A3: X in XX;
X`1 in F & X`2 in G by A3,MCART_1:10;
hence thesis by A2,SETFAM_1:def 4;
end;
let a be object;
assume a in C;
then consider X,Y be set such that
A4: X in AL & Y in BL and
A5: a = X \/ Y by SETFAM_1:def 4;
reconsider X,Y as Subset of T by A4;
set XY = [X,Y];
A6: XY`1 = X & XY`2 = Y;
XY in XX by A4,ZFMISC_1:87;
hence thesis by A5,A6;
end;
card { F(w) where w is Element of A : w in XX } c= card XX from TREES_2:
sch 2;
hence thesis by A1;
end;
theorem Th27:
for F, G being set holds union UNION (F,G) c= union F \/ union G
proof
let F, G be set;
let x be object;
assume x in union UNION (F,G);
then consider Y being set such that
A1: x in Y and
A2: Y in UNION (F,G) by TARSKI:def 4;
consider f,g being set such that
A3: f in F and
A4: g in G and
A5: Y = f \/ g by A2,SETFAM_1:def 4;
per cases by A1,A5,XBOOLE_0:def 3;
suppose
x in f;
then x in union F by A3,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in g;
then x in union G by A4,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th28:
for F, G being set st F <> {} & G <> {} holds union F \/ union G
= union UNION (F,G)
proof
let F, G be set;
assume that
A1: F <> {} and
A2: G <> {};
thus union F \/ union G c= union UNION (F,G)
proof
let x be object;
assume
A3: x in union F \/ union G;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in union F;
consider W being object such that
A5: W in G by A2,XBOOLE_0:def 1;
consider Y being set such that
A6: x in Y and
A7: Y in F by A4,TARSKI:def 4;
reconsider Y,W as set by TARSKI:1;
set YW = Y \/ W;
Y c= YW & YW in UNION (F,G) by A7,A5,SETFAM_1:def 4,XBOOLE_1:7;
hence thesis by A6,TARSKI:def 4;
end;
suppose
A8: x in union G;
consider W being object such that
A9: W in F by A1,XBOOLE_0:def 1;
consider Y being set such that
A10: x in Y and
A11: Y in G by A8,TARSKI:def 4;
reconsider Y,W as set by TARSKI:1;
set YW = W \/ Y;
Y c= YW & YW in UNION (F,G) by A11,A9,SETFAM_1:def 4,XBOOLE_1:7;
hence thesis by A10,TARSKI:def 4;
end;
end;
thus thesis by Th27;
end;
theorem Th29:
for F being set holds UNION ({},F) = {}
proof
let F be set;
UNION ({},F) c= {}
proof
let x be object;
assume x in UNION ({},F);
then ex x1, x2 being set st x1 in {} & x2 in F & x = x1 \/ x2 by
SETFAM_1:def 4;
hence thesis;
end;
hence thesis;
end;
theorem
for F, G being set holds UNION (F, G) = {} implies F = {} or G = {}
proof
let F, G be set;
assume
A1: UNION (F,G) = {};
assume that
A2: F <> {} and
A3: G <> {};
consider X being object such that
A4: X in F by A2,XBOOLE_0:def 1;
consider Y being object such that
A5: Y in G by A3,XBOOLE_0:def 1;
reconsider Y,X as set by TARSKI:1;
X \/ Y in UNION (F,G) by A4,A5,SETFAM_1:def 4;
hence thesis by A1;
end;
theorem
for F, G being set st INTERSECTION (F, G) = {} holds F = {} or G = {}
proof
let F, G be set;
assume that
A1: INTERSECTION (F,G) = {} and
A2: F <> {} and
A3: G <> {};
consider X being object such that
A4: X in F by A2,XBOOLE_0:def 1;
consider Y being object such that
A5: Y in G by A3,XBOOLE_0:def 1;
reconsider Y,X as set by TARSKI:1;
X /\ Y in INTERSECTION (F,G) by A4,A5,SETFAM_1:def 5;
hence thesis by A1;
end;
theorem Th32:
for F, G being set holds meet UNION (F,G) c= meet F \/ meet G
proof
let F, G be set;
per cases;
suppose
A1: F <> {} & G <> {};
let x be object;
assume
A2: x in meet UNION (F,G);
assume
A3: not x in meet F \/ meet G;
then not x in meet F by XBOOLE_0:def 3;
then consider Y being set such that
A4: Y in F & not x in Y by A1,SETFAM_1:def 1;
not x in meet G by A3,XBOOLE_0:def 3;
then consider Z being set such that
A5: Z in G & not x in Z by A1,SETFAM_1:def 1;
( not x in Y \/ Z)& Y \/ Z in UNION (F,G) by A4,A5,SETFAM_1:def 4
,XBOOLE_0:def 3;
hence thesis by A2,SETFAM_1:def 1;
end;
suppose
F = {} or G = {};
then UNION (F,G) = {} by Th29;
then meet UNION (F,G) = {} by SETFAM_1:def 1;
hence thesis;
end;
end;
theorem
for F, G being set st F <> {} & G <> {} holds meet UNION(F,G) = meet F
\/ meet G
by Th32,SETFAM_1:29;
theorem Th34:
for F, G being set st F <> {} & G <> {} holds meet F /\ meet G =
meet INTERSECTION(F,G)
proof
let F, G be set;
assume that
A1: F <> {} and
A2: G <> {};
consider y being object such that
A3: y in F by A1,XBOOLE_0:def 1;
reconsider y as set by TARSKI:1;
consider z being object such that
A4: z in G by A2,XBOOLE_0:def 1;
reconsider z as set by TARSKI:1;
A5: meet INTERSECTION(F,G) c= meet F /\ meet G
proof
let x be object such that
A6: x in meet INTERSECTION(F,G);
for Z be set st Z in G holds x in Z
proof
let Z be set;
assume Z in G;
then y /\ Z in INTERSECTION(F,G) by A3,SETFAM_1:def 5;
then x in y /\ Z by A6,SETFAM_1:def 1;
hence thesis by XBOOLE_0:def 4;
end;
then
A7: x in meet G by A2,SETFAM_1:def 1;
for Z be set st Z in F holds x in Z
proof
let Z be set;
assume Z in F;
then Z /\ z in INTERSECTION(F,G) by A4,SETFAM_1:def 5;
then x in Z /\ z by A6,SETFAM_1:def 1;
hence thesis by XBOOLE_0:def 4;
end;
then x in meet F by A1,SETFAM_1:def 1;
hence thesis by A7,XBOOLE_0:def 4;
end;
A8: y /\ z in INTERSECTION(F,G) by A3,A4,SETFAM_1:def 5;
meet F /\ meet G c= meet INTERSECTION (F,G)
proof
let x be object;
assume x in meet F /\ meet G;
then
A9: x in meet F & x in meet G by XBOOLE_0:def 4;
for Z be set st Z in INTERSECTION(F,G) holds x in Z
proof
let Z be set;
assume Z in INTERSECTION(F,G);
then consider Z1,Z2 be set such that
A10: Z1 in F & Z2 in G and
A11: Z = Z1 /\ Z2 by SETFAM_1:def 5;
x in Z1 & x in Z2 by A9,A10,SETFAM_1:def 1;
hence thesis by A11,XBOOLE_0:def 4;
end;
hence thesis by A8,SETFAM_1:def 1;
end;
hence thesis by A5;
end;
begin :: F_sigma and G_delta Types of Subsets
definition
let T be TopSpace, A be Subset of T;
attr A is F_sigma means
ex F being closed countable Subset-Family of T st A = union F;
end;
definition
let T be TopSpace, A be Subset of T;
attr A is G_delta means
ex F being open countable Subset-Family of T st A = meet F;
end;
registration
let T;
cluster empty -> F_sigma G_delta for Subset of T;
coherence
proof let S be Subset of T;
assume S is empty;
then
A1: S = {}T;
thus S is F_sigma
proof
reconsider E = {} as empty Subset-Family of T by Th18;
{}T = union E by ZFMISC_1:2;
hence thesis by A1;
end;
reconsider F = { {}T } as Subset-Family of T;
F is open & {}T = meet F by Th19,SETFAM_1:10;
hence thesis by A1;
end;
end;
theorem Th35:
[#]T is F_sigma
proof
reconsider F = { [#]T } as Subset-Family of T;
F is closed & [#]T = union F by Th20,ZFMISC_1:25;
hence thesis;
end;
theorem Th36:
[#]T is G_delta
proof
reconsider F = { [#]T } as Subset-Family of T;
F is open & [#]T = meet F by Th19,SETFAM_1:10;
hence thesis;
end;
registration
let T;
cluster [#]T -> F_sigma G_delta;
coherence by Th35,Th36;
end;
theorem
A is F_sigma implies A` is G_delta
proof
assume A is F_sigma;
then consider F being closed countable Subset-Family of T such that
A1: A = union F;
per cases;
suppose
A2: F <> {};
set G = COMPLEMENT F;
A3: G is open by TOPS_2:9;
(union F)` = meet COMPLEMENT F by A2,TOPS_2:6;
hence thesis by A1,A3;
end;
suppose
F = {};
then A` = [#]T by A1,ZFMISC_1:2;
hence thesis;
end;
end;
theorem
A is G_delta implies A` is F_sigma
proof
assume A is G_delta;
then consider F being open countable Subset-Family of T such that
A1: A = meet F;
per cases;
suppose
A2: F <> {};
set G = COMPLEMENT F;
A3: G is closed by TOPS_2:10;
(meet F)` = union COMPLEMENT F by A2,TOPS_2:7;
hence thesis by A1,A3;
end;
suppose
F = {};
then A` = [#]T by A1,SETFAM_1:1;
hence thesis;
end;
end;
theorem
A is F_sigma & B is F_sigma implies A /\ B is F_sigma
proof
assume that
A1: A is F_sigma and
A2: B is F_sigma;
consider F being closed countable Subset-Family of T such that
A3: A = union F by A1;
consider G being closed countable Subset-Family of T such that
A4: B = union G by A2;
reconsider H = INTERSECTION (F,G) as Subset-Family of T;
A5: H is closed by Th21;
card H c= card [:F,G:] & [:F,G:] is countable by Th25,CARD_4:7;
then
A6: H is countable by WAYBEL12:1;
A /\ B = union H by A3,A4,SETFAM_1:28;
hence thesis by A5,A6;
end;
theorem
A is F_sigma & B is F_sigma implies A \/ B is F_sigma
proof
assume that
A1: A is F_sigma and
A2: B is F_sigma;
consider F being closed countable Subset-Family of T such that
A3: A = union F by A1;
consider G being closed countable Subset-Family of T such that
A4: B = union G by A2;
reconsider H = UNION (F,G) as Subset-Family of T;
per cases;
suppose
A5: A <> {} & B <> {};
A6: H is closed by Th22;
card H c= card [:F,G:] & [:F,G:] is countable by Th26,CARD_4:7;
then
A7: H is countable by WAYBEL12:1;
A \/ B = union H by A3,A4,A5,Th28,ZFMISC_1:2;
hence thesis by A6,A7;
end;
suppose
A = {};
hence thesis by A2;
end;
suppose
B = {};
hence thesis by A1;
end;
end;
theorem
A is G_delta & B is G_delta implies A \/ B is G_delta
proof
assume that
A1: A is G_delta and
A2: B is G_delta;
consider F being open countable Subset-Family of T such that
A3: A = meet F by A1;
consider G being open countable Subset-Family of T such that
A4: B = meet G by A2;
reconsider H = UNION (F,G) as Subset-Family of T;
per cases;
suppose
A5: F <> {} & G <> {};
A6: meet UNION(F,G) c= meet F \/ meet G by Th32;
meet F \/ meet G c= meet UNION(F,G) by A5,SETFAM_1:29;
then
A7: A \/ B = meet H by A3,A4,A6;
card H c= card [:F,G:] & [:F,G:] is countable by Th26,CARD_4:7;
then
A8: H is countable by WAYBEL12:1;
H is open by Th24;
hence thesis by A7,A8;
end;
suppose
F = {} or G = {};
then A = {} or B = {} by A3,A4,SETFAM_1:def 1;
hence thesis by A1,A2;
end;
end;
theorem
A is G_delta & B is G_delta implies A /\ B is G_delta
proof
assume that
A1: A is G_delta and
A2: B is G_delta;
consider F being open countable Subset-Family of T such that
A3: A = meet F by A1;
consider G being open countable Subset-Family of T such that
A4: B = meet G by A2;
reconsider H = INTERSECTION (F,G) as Subset-Family of T;
per cases;
suppose
A5: F <> {} & G <> {};
A6: H is open by Th23;
card H c= card [:F,G:] & [:F,G:] is countable by Th25,CARD_4:7;
then
A7: H is countable by WAYBEL12:1;
A /\ B = meet H by A3,A4,A5,Th34;
hence thesis by A6,A7;
end;
suppose
F = {} or G = {};
then A = {} or B = {} by A3,A4,SETFAM_1:def 1;
then A /\ B = {}T;
hence thesis;
end;
end;
theorem
for A being Subset of T st A is closed holds A is F_sigma
proof
let A be Subset of T;
assume A is closed;
then reconsider F = {A} as closed countable Subset-Family of T by Th20;
take F;
thus thesis by ZFMISC_1:25;
end;
theorem
for A being Subset of T st A is open holds A is G_delta
proof
let A be Subset of T;
assume A is open;
then reconsider F = {A} as open countable Subset-Family of T by Th19;
take F;
thus thesis by SETFAM_1:10;
end;
theorem
for A being Subset of R^1 st A = RAT holds A is F_sigma
proof
defpred R[object] means ex a being Element of RAT st a = $1;
defpred P[object] means ex a being Element of RAT st {a} = $1;
let A be Subset of R^1;
ex F being set st for x being set holds x in F iff x in bool RAT & P[x]
from XFAMILY:sch 1;
then consider F being set such that
A1: for x being set holds x in F iff x in bool RAT & P[x];
A2: bool RAT c= bool REAL by NUMBERS:12,ZFMISC_1:67;
F c= bool the carrier of R^1
by A1,A2,TOPMETR:17;
then reconsider F as Subset-Family of R^1;
assume
A3: A = RAT;
ex F being Subset-Family of R^1 st F is closed countable & A = union F
proof
take F;
for B being Subset of R^1 st B in F holds B is closed
proof
let B be Subset of R^1;
assume B in F;
then ex a being Element of RAT st {a} = B by A1;
hence thesis;
end;
hence F is closed by TOPS_2:def 2;
A4: F = { {x} where x is Element of RAT : R[x] }
proof
thus F c= { {x} where x is Element of RAT : R[x] }
proof
let y be object;
assume y in F;
then P[y] by A1;
hence thesis;
end;
let y be object;
assume y in { {x} where x is Element of RAT : R[x] };
then ex z being Element of RAT st y = {z} & R[z];
hence thesis by A1;
end;
{ {x} where x is Element of RAT : R[x] } is countable from
FraenCoun11;
hence F is countable by A4;
thus A c= union F
proof
let x be object;
assume x in A;
then reconsider x as Element of RAT by A3;
{x} in F & x in {x} by A1,TARSKI:def 1;
hence thesis by TARSKI:def 4;
end;
let x be object;
assume x in union F;
then consider Y being set such that
A5: x in Y and
A6: Y in F by TARSKI:def 4;
ex a being Element of RAT st {a} = Y by A1,A6;
hence thesis by A3,A5;
end;
hence thesis;
end;
begin :: T_1/2 Topological Spaces
definition
let T be TopSpace;
attr T is T_1/2 means
for A being Subset of T holds Der A is closed;
end;
theorem Th46:
for T being TopSpace st T is T_1 holds T is T_1/2
proof
let T be TopSpace;
assume
A1: T is T_1;
for A being Subset of T holds Der A is closed
proof
let A be Subset of T;
Der A = Cl Der A by A1,TOPGEN_1:33;
hence thesis;
end;
hence thesis;
end;
theorem Th47:
for T being non empty TopSpace st T is T_1/2 holds T is T_0
proof
let T be non empty TopSpace;
assume
A1: T is T_1/2;
now
let x, y be Point of T;
assume
A2: x <> y;
assume that
A3: x in Cl {y} and
A4: y in Cl {x};
not for G being Subset of T st G is open holds y in G implies {x} meets G
proof
set X = (Der {x})`;
not x in Der {x}
proof
set U = the a_neighborhood of x;
consider V being Subset of T such that
A5: V is open and
V c= U and
A6: x in V by CONNSP_2:6;
assume x in Der {x};
then consider z being Point of T such that
A7: z in {x} /\ V and
A8: x <> z by A5,A6,TOPGEN_1:17;
z in {x} by A7,XBOOLE_0:def 4;
hence thesis by A8,TARSKI:def 1;
end;
then
A9: x in (Der {x})` by SUBSET_1:29;
assume
A10: for G being Subset of T st G is open holds y in G implies {x} meets G;
for U being open Subset of T st y in U ex r being Point of T st r in
{x} /\ U & y <> r
proof
let U be open Subset of T;
assume y in U;
then {x} meets U by A10;
then
A11: x in U by ZFMISC_1:50;
x in {x} by TARSKI:def 1;
then x in {x} /\ U by A11,XBOOLE_0:def 4;
hence thesis by A2;
end;
then y in Der {x} by TOPGEN_1:17;
then
A12: not y in X by XBOOLE_0:def 5;
Der {x} is closed by A1;
then {y} meets X by A3,A9,PRE_TOPC:24;
hence thesis by A12,ZFMISC_1:50;
end;
hence contradiction by A4,PRE_TOPC:24;
end;
hence thesis by TSP_1:def 6;
end;
registration
cluster T_1/2 -> T_0 for TopSpace;
coherence
proof
let T be TopSpace;
per cases;
suppose
T is non empty;
then reconsider T9 = T as non empty TopSpace;
assume T is T_1/2;
then T9 is T_1/2;
hence thesis by Th47;
end;
suppose
T is empty;
then reconsider T9 = T as empty TopSpace;
T9 is T_0;
hence thesis;
end;
end;
cluster T_1 -> T_1/2 for TopSpace;
coherence by Th46;
end;
begin :: Condensation Points
:: Page 77 - 1.7.11
definition
let T, A;
let x be Point of T;
pred x is_a_condensation_point_of A means
for N being a_neighborhood of x holds N /\ A is not countable;
end;
reserve x for Point of T;
theorem Th48:
x is_a_condensation_point_of A & A c= B implies x
is_a_condensation_point_of B
proof
assume that
A1: x is_a_condensation_point_of A and
A2: A c= B;
for N being a_neighborhood of x holds N /\ B is not countable
proof
let N be a_neighborhood of x;
N /\ A c= N /\ B by A2,XBOOLE_1:26;
hence thesis by A1;
end;
hence thesis;
end;
definition
let T, A;
func A^0 -> Subset of T means
:Def10:
for x being Point of T holds x in it iff x is_a_condensation_point_of A;
existence
proof
defpred P[Point of T] means $1 is_a_condensation_point_of A;
ex X being Subset of T st for x being Element of T holds x in X iff P[x
] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[Point of T] means $1 is_a_condensation_point_of A;
let A1, A2 be Subset of T such that
A1: for x being Element of T holds x in A1 iff P[x] and
A2: for x being Element of T holds x in A2 iff P[x];
thus A1 = A2 from SUBSET_1:sch 2(A1,A2);
end;
end;
theorem Th49:
for p being Point of T st p is_a_condensation_point_of A holds p
is_an_accumulation_point_of A
proof
let p be Point of T;
assume
A1: p is_a_condensation_point_of A;
for U being open Subset of T st p in U ex q being Point of T st q <> p &
q in A & q in U
proof
let U be open Subset of T;
assume p in U;
then reconsider N = U as a_neighborhood of p by CONNSP_2:3;
reconsider NU = N /\ A as non empty non countable set by A1;
consider q being Element of NU such that
A2: p <> q by SUBSET_1:50;
q in NU;
then reconsider q as Point of T;
q in A & q in U by XBOOLE_0:def 4;
hence thesis by A2;
end;
hence thesis by TOPGEN_1:21;
end;
theorem
A^0 c= Der A
proof
let x be object;
assume
A1: x in A^0;
then reconsider p = x as Point of T;
p is_a_condensation_point_of A by A1,Def10;
then p is_an_accumulation_point_of A by Th49;
hence thesis by TOPGEN_1:16;
end;
theorem
A^0 = Cl (A^0)
proof
thus A^0 c= Cl (A^0) by PRE_TOPC:18;
let x be object;
assume
A1: x in Cl (A^0);
then reconsider p = x as Point of T;
for N being a_neighborhood of p holds N /\ A is not countable
proof
let N be a_neighborhood of p;
consider N1 being Subset of T such that
A2: N1 is open and
A3: N1 c= N and
A4: p in N1 by CONNSP_2:6;
A^0 meets N1 by A1,A2,A4,PRE_TOPC:24;
then consider y being object such that
A5: y in A^0 and
A6: y in N1 by XBOOLE_0:3;
reconsider y9 = y as Point of T by A5;
reconsider N1 as a_neighborhood of y9 by A2,A6,CONNSP_2:6;
A7: N1 /\ A c= N /\ A by A3,XBOOLE_1:26;
y9 is_a_condensation_point_of A by A5,Def10;
hence thesis by A7;
end;
then p is_a_condensation_point_of A;
hence thesis by Def10;
end;
theorem Th52:
A c= B implies A^0 c= B^0
proof
assume
A1: A c= B;
let x be object;
assume
A2: x in A^0;
then reconsider x9 = x as Point of T;
x9 is_a_condensation_point_of A by A2,Def10;
then x9 is_a_condensation_point_of B by A1,Th48;
hence thesis by Def10;
end;
theorem Th53:
x is_a_condensation_point_of A \/ B implies x
is_a_condensation_point_of A or x is_a_condensation_point_of B
proof
assume
A1: x is_a_condensation_point_of A \/ B;
assume that
A2: not x is_a_condensation_point_of A and
A3: not x is_a_condensation_point_of B;
consider N1 being a_neighborhood of x such that
A4: N1 /\ A is countable by A2;
consider N2 being a_neighborhood of x such that
A5: N2 /\ B is countable by A3;
reconsider N3 = N1 /\ N2 as a_neighborhood of x by CONNSP_2:2;
N3 /\ A c= N1 /\ A & N3 /\ B c= N2 /\ B by XBOOLE_1:17,26;
then (N3 /\ A) \/ (N3 /\ B) is countable by A4,A5,CARD_2:85;
then N3 /\ (A \/ B) is countable by XBOOLE_1:23;
hence thesis by A1;
end;
theorem
(A \/ B)^0 = (A^0) \/ (B^0)
proof
thus (A \/ B)^0 c= (A^0) \/ (B^0)
proof
let x be object;
assume
A1: x in (A \/ B)^0;
then reconsider x9 = x as Point of T;
x9 is_a_condensation_point_of A \/ B by A1,Def10;
then
x9 is_a_condensation_point_of A or x9 is_a_condensation_point_of B by Th53;
then x9 in A^0 or x9 in B^0 by Def10;
hence thesis by XBOOLE_0:def 3;
end;
A^0 c= (A \/ B)^0 & B^0 c= (A \/ B)^0 by Th52,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem Th55:
A is countable implies not ex x being Point of T st x
is_a_condensation_point_of A
proof
assume
A1: A is countable;
given x being Point of T such that
A2: x is_a_condensation_point_of A;
set N = the a_neighborhood of x;
N /\ A is not countable by A2;
hence thesis by A1,CARD_3:94;
end;
theorem Th56:
A is countable implies A^0 = {}
proof
assume
A1: A is countable;
assume A^0 <> {};
then consider x being object such that
A2: x in A^0 by XBOOLE_0:def 1;
reconsider x9 = x as Point of T by A2;
x9 is_a_condensation_point_of A by A2,Def10;
hence thesis by A1,Th55;
end;
registration
let T;
let A be countable Subset of T;
cluster A^0 -> empty;
coherence by Th56;
end;
theorem
T is second-countable implies ex B being Basis of T st B is countable
proof
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= B and
A1: card B1 = weight T by TOPGEN_2:18;
assume T is second-countable;
then card B1 c= omega by A1,WAYBEL23:def 6;
then card card B1 c= card omega;
then B1 is countable;
hence thesis;
end;
registration
cluster second-countable non empty for TopSpace;
existence
proof
set T = the finite non empty TopSpace;
take T;
thus thesis;
end;
end;
begin :: Borel Families of Subsets
registration
let T;
cluster TotFam T -> non empty all-open-containing compl-closed
closed_for_countable_unions;
coherence;
end;
theorem
for T being set, A being SetSequence of T holds
rng A is countable non empty Subset-Family of T
proof
let T be set, A be SetSequence of T;
A.1 in rng A by FUNCT_2:4;
then reconsider AA = rng A as non empty Subset-Family of T;
card rng A c= card dom A & dom A is countable by CARD_2:61,FUNCT_2:def 1;
then AA is countable by WAYBEL12:1;
hence thesis;
end;
theorem Th59:
for F, G being Subset-Family of T st F is all-open-containing &
F c= G holds G is all-open-containing;
theorem
for F, G being Subset-Family of T st F is all-closed-containing & F c=
G holds G is all-closed-containing;
definition
let T be 1-sorted;
mode SigmaField of T is SigmaField of the carrier of T;
end;
registration
let T be non empty TopSpace;
cluster compl-closed closed_for_countable_unions closed_for_countable_meets
all-closed-containing all-open-containing for Subset-Family of T;
existence
proof
take TotFam T;
thus thesis;
end;
end;
theorem Th61:
sigma TotFam T is all-open-containing compl-closed
closed_for_countable_unions
proof
set E = sigma TotFam T;
TotFam T c= sigma TotFam T by PROB_1:def 9;
hence E is all-open-containing;
thus E is compl-closed;
thus thesis;
end;
registration
let T;
cluster sigma TotFam T -> all-open-containing compl-closed
closed_for_countable_unions;
coherence by Th61;
end;
registration
let T be non empty 1-sorted;
cluster sigma-additive compl-closed closed_for_countable_unions non empty
for Subset-Family of T;
existence
proof
take sigma TotFam T;
thus thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster -> closed_for_countable_unions for SigmaField of T;
coherence;
end;
theorem
for T being non empty TopSpace, F being Subset-Family of T st F is
compl-closed closed_for_countable_unions holds F is SigmaField of T by Th13;
registration
let T be non empty TopSpace;
cluster all-open-containing for SigmaField of T;
existence
proof
take sigma TotFam T;
thus thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster Topology_of T -> open all-open-containing;
coherence
by PRE_TOPC:def 2;
end;
theorem Th63:
for X being Subset-Family of T ex Y being all-open-containing
compl-closed closed_for_countable_unions Subset-Family of T st X c= Y & for Z
be all-open-containing compl-closed closed_for_countable_unions Subset-Family
of T st X c= Z holds Y c= Z
proof
let X be Subset-Family of T;
set V = { S where S is Subset-Family of T : X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
};
set Y = meet V;
A1: now
let Z be set;
assume Z in V;
then ex S be Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
;
hence X c= Z;
end;
A2: bool the carrier of T in V
proof
set X1 = TotFam T;
X1 in V;
hence thesis;
end;
A3: for E being Subset of T st E in Y holds E` in Y
proof
let E be Subset of T such that
A4: E in Y;
now
let Z be set;
assume Z in V;
then E in Z & ex S being Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
by A4,SETFAM_1:def 1;
hence E` in Z by PROB_1:def 1;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
A5: for BSeq be SetSequence of the carrier of T st rng BSeq c= Y holds
Intersection BSeq in Y
proof
let BSeq be SetSequence of the carrier of T such that
A6: rng BSeq c= Y;
now
let Z be set;
assume
A7: Z in V;
then consider S be Subset-Family of T such that
A8: Z = S and
X c= S and
A9: S is all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T;
now
let n be Nat;
BSeq.n in rng BSeq by NAT_1:51;
hence BSeq.n in Z by A6,A7,SETFAM_1:def 1;
end;
then
A10: rng BSeq c= Z by NAT_1:52;
S is SigmaField of T by A9,Th13;
hence Intersection BSeq in Z by A8,A10,PROB_1:def 6;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
now
let Z be set;
assume Z in V;
then ex S being Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
;
then Z is Field_Subset of the carrier of T by Th13;
hence {} in Z by PROB_1:4;
end;
then {} in Y by A2,SETFAM_1:def 1;
then reconsider Y as SigmaField of T by A2,A5,A3,PROB_1:15,SETFAM_1:3;
for A being Subset of T st A is open holds A in Y
proof
let A be Subset of T;
assume
A11: A is open;
for Y being set holds Y in V implies A in Y
proof
let Y be set;
assume Y in V;
then ex S being Subset-Family of the carrier of T st Y = S & X c= S & S
is all-open-containing compl-closed closed_for_countable_unions Subset-Family
of T;
hence thesis by A11,Def2;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
then reconsider
Y as all-open-containing compl-closed closed_for_countable_unions
Subset-Family of T by Def2;
take Y;
for Z be set st X c= Z & Z is all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T holds Y c= Z
proof
let Z be set;
assume that
A12: X c= Z and
A13: Z is all-open-containing compl-closed closed_for_countable_unions
Subset-Family of T;
reconsider Z as Subset-Family of T by A13;
Z in V by A12,A13;
hence thesis by SETFAM_1:3;
end;
hence thesis by A2,A1,SETFAM_1:5;
end;
definition
let T;
func BorelSets T -> all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T means
:Def11:
for G being
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
holds it c= G;
existence
proof
reconsider E = {} as Subset-Family of T by Th18;
consider Y being all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T such that
E c= Y and
A1: for Z be all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T st E c= Z holds Y c= Z by Th63;
take Y;
let G be all-open-containing compl-closed closed_for_countable_unions
Subset-Family of T;
thus thesis by A1,XBOOLE_1:2;
end;
uniqueness;
end;
theorem Th64:
for F being closed Subset-Family of T holds F c= BorelSets T
proof
let F be closed Subset-Family of T;
F c= BorelSets T
proof
let x be object;
assume
A1: x in F;
then reconsider xx = x as Subset of T;
xx is closed by A1,TOPS_2:def 2;
hence thesis by Def3;
end;
hence thesis;
end;
theorem Th65:
for F being open Subset-Family of T holds F c= BorelSets T
proof
let F be open Subset-Family of T;
F c= BorelSets T
proof
let x be object;
assume
A1: x in F;
then reconsider xx = x as Subset of T;
xx is open by A1,TOPS_2:def 1;
hence thesis by Def2;
end;
hence thesis;
end;
theorem
BorelSets T = sigma Topology_of T
proof
reconsider BT = BorelSets T as SigmaField of T by Th13;
set X = Topology_of T;
A1: for Z being set st X c= Z & Z is SigmaField of T holds BT c= Z
proof
let Z be set;
assume that
A2: X c= Z and
A3: Z is SigmaField of T;
reconsider Z9 = Z as SigmaField of T by A3;
Z9 is all-open-containing by A2,Th59;
hence thesis by Def11;
end;
X c= BT by Th65;
hence thesis by A1,PROB_1:def 9;
end;
definition
let T, A;
attr A is Borel means
A in BorelSets T;
end;
registration
let T;
cluster F_sigma -> Borel for Subset of T;
coherence
by Th64,Def4;
end;
registration
let T;
cluster G_delta -> Borel for Subset of T;
coherence
by Th65,Def5;
end;