:: TOPGEN_4 semantic presentation
begin
definition
let T be 1-sorted ;
func TotFam T -> Subset-Family of T equals :: TOPGEN_4:def 1
bool the carrier of T;
coherence
bool the carrier of T is Subset-Family of T by ZFMISC_1:def_1;
end;
:: deftheorem defines TotFam TOPGEN_4:def_1_:_
for T being 1-sorted holds TotFam T = bool the carrier of T;
theorem Th1: :: TOPGEN_4:1
for T being set
for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
proof
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
let F be Subset-Family of T; ::_thesis: ( F is countable iff COMPLEMENT F is countable )
F, COMPLEMENT F are_equipotent by YELLOW_8:3;
hence ( F is countable iff COMPLEMENT F is countable ) by YELLOW_8:4; ::_thesis: verum
end;
registration
cluster RAT -> countable ;
coherence
RAT is countable by CARD_3:def_14, 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 ) )
proof
let X be set ; ::_thesis: ( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
thus ( X is countable implies ex f being Function st
( dom f = RAT & X c= rng f ) ) ::_thesis: ( ex f being Function st
( dom f = RAT & X c= rng f ) implies X is countable )
proof
assume card X c= omega ; :: according to CARD_3:def_14 ::_thesis: ex f being Function st
( dom f = RAT & X c= rng f )
hence ex f being Function st
( dom f = RAT & X c= rng f ) by CARD_1:12, TOPGEN_3:17; ::_thesis: verum
end;
assume ex f being Function st
( dom f = RAT & X c= rng f ) ; ::_thesis: X is countable
hence card X c= omega by CARD_1:12, TOPGEN_3:17; :: according to CARD_3:def_14 ::_thesis: verum
end;
scheme :: TOPGEN_4:sch 1
FraenCoun11{ P1[ set ] } :
{ {n} where n is Element of RAT : P1[n] } is countable
proof
deffunc H1( set ) -> set = {$1};
consider f being Function such that
A1: ( dom f = RAT & ( for x being set st x in RAT holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
{ {n} where n is Element of RAT : P1[n] } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {n} where n is Element of RAT : P1[n] } or x in rng f )
assume x in { {n} where n is Element of RAT : P1[n] } ; ::_thesis: x in rng f
then consider n being Element of RAT such that
A2: x = {n} and
P1[n] ;
f . n = x by A1, A2;
hence x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum
end;
hence { {n} where n is Element of RAT : P1[n] } is countable by A1, Lm1; ::_thesis: verum
end;
theorem :: TOPGEN_4:2
for T being non empty TopSpace
for 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; ::_thesis: for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }
let A be Subset of T; ::_thesis: Der A = { x where x is Point of T : x in Cl (A \ {x}) }
thus Der A c= { x where x is Point of T : x in Cl (A \ {x}) } :: according to XBOOLE_0:def_10 ::_thesis: { x where x is Point of T : x in Cl (A \ {x}) } c= Der A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der A or x in { x where x is Point of T : x in Cl (A \ {x}) } )
assume x in Der A ; ::_thesis: x in { x where x is Point of T : x in Cl (A \ {x}) }
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 x in { x where x is Point of T : x in Cl (A \ {x}) } ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Point of T : x in Cl (A \ {x}) } or y in Der A )
assume y in { x where x is Point of T : x in Cl (A \ {x}) } ; ::_thesis: y in Der A
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 y in Der A by A1, TOPGEN_1:def_3; ::_thesis: verum
end;
registration
cluster finite -> second-countable for TopStruct ;
coherence
for b1 being TopStruct st b1 is finite holds
b1 is second-countable
proof
let T be TopStruct ; ::_thesis: ( T is finite implies T is second-countable )
assume T is finite ; ::_thesis: T is second-countable
then reconsider T9 = T as finite TopStruct ;
weight T9 is finite by TOPGEN_2:def_4;
then weight T9 c= omega ;
hence T is second-countable by WAYBEL23:def_6; ::_thesis: verum
end;
end;
registration
cluster REAL -> non countable ;
coherence
not REAL is countable
proof
assume REAL is countable ; ::_thesis: contradiction
then card REAL c= omega by CARD_3:def_14;
hence contradiction by TOPGEN_3:30, TOPGEN_3:def_4; ::_thesis: verum
end;
end;
registration
cluster non countable -> non finite for set ;
coherence
for b1 being set st not b1 is countable holds
not b1 is finite ;
cluster non finite -> non trivial for set ;
coherence
for b1 being set st not b1 is finite holds
not b1 is trivial ;
cluster non empty non countable for set ;
existence
ex b1 being set st
( not b1 is countable & not b1 is empty )
proof
take REAL ; ::_thesis: ( not REAL is countable & not REAL is empty )
thus ( not REAL is countable & not REAL is empty ) ; ::_thesis: verum
end;
end;
theorem :: TOPGEN_4:3
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff Der A c= A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds
( A is closed iff Der A c= A )
let A be Subset of T; ::_thesis: ( A is closed iff Der A c= A )
hereby ::_thesis: ( Der A c= A implies A is closed )
assume A is closed ; ::_thesis: Der A c= A
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; ::_thesis: verum
end;
assume A2: Der A c= A ; ::_thesis: A is closed
Cl A = A \/ (Der A) by TOPGEN_1:29
.= A by A2, XBOOLE_1:12 ;
hence A is closed ; ::_thesis: verum
end;
theorem Th4: :: TOPGEN_4:4
for T being non empty TopStruct
for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
proof
let T be non empty TopStruct ; ::_thesis: for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
let B be Basis of T; ::_thesis: for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
let V be Subset of T; ::_thesis: ( V is open & V <> {} implies ex W being Subset of T st
( W in B & W c= V & W <> {} ) )
assume that
A1: V is open and
A2: V <> {} ; ::_thesis: ex W being Subset of T st
( W in B & W c= V & W <> {} )
consider x being set 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 ex W being Subset of T st
( W in B & W c= V & W <> {} ) by A4; ::_thesis: verum
end;
begin
theorem Th5: :: TOPGEN_4:5
for T being non empty TopSpace holds density T c= weight T
proof
let T be non empty TopSpace; ::_thesis: density T c= weight T
defpred S1[ set ] means $1 <> {} ;
deffunc H1( set ) -> Element of $1 = choose $1;
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
set A = { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } ;
{ H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } or x in the carrier of T )
assume x in { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } ; ::_thesis: x in the carrier of T
then consider B2 being Subset of T such that
A2: x = choose B2 and
B2 in B1 and
A3: B2 <> {} ;
x in B2 by A2, A3;
hence x in the carrier of T ; ::_thesis: verum
end;
then reconsider A = { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } 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; ::_thesis: ( Q <> {} & Q is open implies A meets Q )
assume ( Q <> {} & Q is open ) ; ::_thesis: A meets Q
then consider W being Subset of T such that
A4: W in B1 and
A5: W c= Q and
A6: W <> {} by Th4;
( choose W in A & choose W in W ) by A4, A6;
hence A meets Q by A5, XBOOLE_0:3; ::_thesis: verum
end;
then A is dense by TOPS_1:45;
then A7: density T c= card A by TOPGEN_1:def_12;
card { H1(w) where w is Element of bool the carrier of T : ( w in B1 & S1[w] ) } c= card B1 from BORSUK_2:sch_1();
hence density T c= weight T by A1, A7, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TOPGEN_4:6
for T being non empty TopSpace holds
( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )
proof
let T be non empty TopSpace; ::_thesis: ( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )
hereby ::_thesis: ( ex A being Subset of T st
( A is dense & A is countable ) implies T is separable )
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 ; ::_thesis: ex A being Subset of T st
( A is dense & A is countable )
then density T c= omega by TOPGEN_1:def_13;
then A is countable by A2, CARD_3:def_14;
hence ex A being Subset of T st
( A is dense & A is countable ) by A1; ::_thesis: verum
end;
given A being Subset of T such that A3: ( A is dense & A is countable ) ; ::_thesis: T is separable
( density T c= card A & card A c= omega ) by A3, CARD_3:def_14, TOPGEN_1:def_12;
then density T c= omega by XBOOLE_1:1;
hence T is separable by TOPGEN_1:def_13; ::_thesis: verum
end;
theorem Th7: :: TOPGEN_4:7
for T being non empty TopSpace st T is second-countable holds
T is separable
proof
let T be non empty TopSpace; ::_thesis: ( T is second-countable implies T is separable )
assume T is second-countable ; ::_thesis: T is separable
then A1: weight T c= omega by WAYBEL23:def_6;
density T c= weight T by Th5;
then density T c= omega by A1, XBOOLE_1:1;
hence T is separable by TOPGEN_1:def_13; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like second-countable -> non empty separable for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is second-countable holds
b1 is separable by Th7;
end;
theorem :: TOPGEN_4:8
for T being non empty TopSpace
for 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; ::_thesis: for A, B being Subset of T st A,B are_separated holds
Fr (A \/ B) = (Fr A) \/ (Fr B)
let A, B be Subset of T; ::_thesis: ( A,B are_separated implies Fr (A \/ B) = (Fr A) \/ (Fr B) )
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 ; ::_thesis: Fr (A \/ B) = (Fr A) \/ (Fr B)
then A3: A misses Cl B by CONNSP_1:def_1;
A misses B by A2, CONNSP_1:1;
then A4: A /\ B = {} by XBOOLE_0:def_7;
A5: Cl A misses B by A2, CONNSP_1:def_1;
A6: (Fr A) \/ (Fr B) c= Fr (A \/ B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Fr A) \/ (Fr B) or x in Fr (A \/ B) )
assume A7: x in (Fr A) \/ (Fr B) ; ::_thesis: x in Fr (A \/ B)
percases ( x in Fr (A \/ B) or x in (Fr A) /\ (Fr B) ) by A4, A1, A7, XBOOLE_0:def_3;
suppose x in Fr (A \/ B) ; ::_thesis: x in Fr (A \/ B)
hence x in Fr (A \/ B) ; ::_thesis: verum
end;
supposeA8: x in (Fr A) /\ (Fr B) ; ::_thesis: x in Fr (A \/ 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 x in Fr (A \/ B) by TOPS_1:def_2; ::_thesis: verum
end;
end;
end;
Fr (A \/ B) c= (Fr A) \/ (Fr B) by TOPS_1:33;
hence Fr (A \/ B) = (Fr A) \/ (Fr B) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPGEN_4:9
for T being non empty TopSpace
for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)
let F be Subset-Family of T; ::_thesis: ( F is locally_finite implies Fr (union F) c= union (Fr F) )
assume F is locally_finite ; ::_thesis: Fr (union F) c= union (Fr F)
then A1: Cl (union F) = union (clf F) by PCOMPS_1:20;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (union F) or x in union (Fr F) )
assume x in Fr (union F) ; ::_thesis: x in union (Fr 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 x in union (Fr F) by A8, TARSKI:def_4; ::_thesis: verum
end;
theorem Th10: :: TOPGEN_4:10
for T being non empty discrete TopSpace holds
( T is separable iff card ([#] T) c= omega )
proof
let T be non empty discrete TopSpace; ::_thesis: ( T is separable iff card ([#] T) c= omega )
hereby ::_thesis: ( card ([#] T) c= omega implies T is separable )
assume T is separable ; ::_thesis: card ([#] T) c= omega
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; ::_thesis: verum
end;
assume card ([#] T) c= omega ; ::_thesis: T is separable
then T is countable by TOPGEN_1:2;
hence T is separable ; ::_thesis: verum
end;
theorem :: TOPGEN_4:11
for T being non empty discrete TopSpace holds
( T is separable iff T is countable )
proof
let T be non empty discrete TopSpace; ::_thesis: ( T is separable iff T is countable )
( T is separable iff card ([#] T) c= omega ) by Th10;
hence ( T is separable iff T is countable ) by TOPGEN_1:2; ::_thesis: verum
end;
begin
definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attrF is all-open-containing means :Def2: :: TOPGEN_4:def 2
for A being Subset of T st A is open holds
A in F;
end;
:: deftheorem Def2 defines all-open-containing TOPGEN_4:def_2_:_
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-open-containing iff for A being Subset of T st A is open holds
A in F );
definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attrF is all-closed-containing means :Def3: :: TOPGEN_4:def 3
for A being Subset of T st A is closed holds
A in F;
end;
:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def_3_:_
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing iff for A being Subset of T st A is closed holds
A in F );
definition
let T be set ;
let F be Subset-Family of T;
attrF is closed_for_countable_unions means :Def4: :: TOPGEN_4:def 4
for G being countable Subset-Family of T st G c= F holds
union G in F;
end;
:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def_4_:_
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_unions iff for G being countable Subset-Family of T st G c= F holds
union G in F );
Lm2: for T being set
for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
let F be Subset-Family of T; ::_thesis: ( F is SigmaField of T implies F is closed_for_countable_unions )
assume A1: F is SigmaField of T ; ::_thesis: F is closed_for_countable_unions
let G be countable Subset-Family of T; :: according to TOPGEN_4:def_4 ::_thesis: ( G c= F implies union G in F )
assume A2: G c= F ; ::_thesis: union G in F
percases ( G is empty or not G is empty ) ;
suppose G is empty ; ::_thesis: union G in F
hence union G in F by A1, PROB_1:4, ZFMISC_1:2; ::_thesis: verum
end;
suppose not G is empty ; ::_thesis: union G in F
hence union G in F by A1, A2, MEASURE1:def_5; ::_thesis: verum
end;
end;
end;
registration
let T be set ;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions for Element of bool (bool T);
coherence
for b1 being SigmaField of T holds b1 is closed_for_countable_unions by Lm2;
end;
theorem Th12: :: TOPGEN_4:12
for T being set
for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F
let F be Subset-Family of T; ::_thesis: ( F is closed_for_countable_unions implies {} in F )
reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;
A1: E c= F by XBOOLE_1:2;
assume F is closed_for_countable_unions ; ::_thesis: {} in F
hence {} in F by A1, Def4, ZFMISC_1:2; ::_thesis: verum
end;
registration
let T be set ;
cluster closed_for_countable_unions -> non empty for Element of bool (bool T);
coherence
for b1 being Subset-Family of T st b1 is closed_for_countable_unions holds
not b1 is empty by Th12;
end;
theorem Th13: :: TOPGEN_4:13
for T being set
for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
proof
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
let F be Subset-Family of T; ::_thesis: ( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
thus ( F is SigmaField of T implies ( F is compl-closed & F is closed_for_countable_unions ) ) ; ::_thesis: ( F is compl-closed & F is closed_for_countable_unions implies F is SigmaField of T )
assume A1: ( F is compl-closed & F is closed_for_countable_unions ) ; ::_thesis: F is SigmaField of T
F is sigma-additive
proof
let M be N_Sub_set_fam of T; :: according to MEASURE1:def_5 ::_thesis: ( not M c= F or union M in F )
assume M c= F ; ::_thesis: union M in F
hence union M in F by A1, Def4; ::_thesis: verum
end;
then reconsider F = F as non empty compl-closed sigma-additive Subset-Family of T by A1;
F is SigmaField of T ;
hence F is SigmaField of T ; ::_thesis: verum
end;
definition
let T be set ;
let F be Subset-Family of T;
attrF is closed_for_countable_meets means :Def5: :: TOPGEN_4:def 5
for G being countable Subset-Family of T st G c= F holds
meet G in F;
end;
:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def_5_:_
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets iff for G being countable Subset-Family of T st G c= F holds
meet G in F );
theorem Th14: :: TOPGEN_4:14
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
let F be Subset-Family of T; ::_thesis: ( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
hereby ::_thesis: ( F is all-open-containing & F is compl-closed implies ( F is all-closed-containing & F is compl-closed ) )
assume A1: ( F is all-closed-containing & F is compl-closed ) ; ::_thesis: ( F is all-open-containing & F is compl-closed )
for A being Subset of T st A is open holds
A in F
proof
let A be Subset of T; ::_thesis: ( A is open implies A in F )
assume A is open ; ::_thesis: A in F
then A ` in F by A1, Def3;
then (A `) ` in F by A1, PROB_1:def_1;
hence A in F ; ::_thesis: verum
end;
hence ( F is all-open-containing & F is compl-closed ) by A1, Def2; ::_thesis: verum
end;
assume A2: ( F is all-open-containing & F is compl-closed ) ; ::_thesis: ( F is all-closed-containing & F is compl-closed )
for A being Subset of T st A is closed holds
A in F
proof
let A be Subset of T; ::_thesis: ( A is closed implies A in F )
assume A is closed ; ::_thesis: A in F
then A ` in F by A2, Def2;
then (A `) ` in F by A2, PROB_1:def_1;
hence A in F ; ::_thesis: verum
end;
hence ( F is all-closed-containing & F is compl-closed ) by A2, Def3; ::_thesis: verum
end;
theorem :: TOPGEN_4:15
for T being set
for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
let F be Subset-Family of T; ::_thesis: ( F is compl-closed implies F = COMPLEMENT F )
assume A1: F is compl-closed ; ::_thesis: F = COMPLEMENT F
thus F c= COMPLEMENT F :: according to XBOOLE_0:def_10 ::_thesis: COMPLEMENT F c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in COMPLEMENT F )
assume A2: x in F ; ::_thesis: x in COMPLEMENT F
then reconsider x9 = x as Subset of T ;
x9 ` in F by A1, A2, PROB_1:def_1;
hence x in COMPLEMENT F by SETFAM_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT F or x in F )
assume A3: x in COMPLEMENT F ; ::_thesis: x in F
then reconsider x9 = x as Subset of T ;
x9 ` in F by A3, SETFAM_1:def_7;
then (x9 `) ` in F by A1, PROB_1:def_1;
hence x in F ; ::_thesis: verum
end;
theorem Th16: :: TOPGEN_4:16
for T being set
for 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 ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is compl-closed holds
COMPLEMENT F c= G
let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is compl-closed implies COMPLEMENT F c= G )
assume A1: ( F c= G & G is compl-closed ) ; ::_thesis: COMPLEMENT F c= G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT F or x in G )
assume A2: x in COMPLEMENT F ; ::_thesis: x in G
then reconsider x9 = x as Subset of T ;
x9 ` in F by A2, SETFAM_1:def_7;
then (x9 `) ` in G by A1, PROB_1:def_1;
hence x in G ; ::_thesis: verum
end;
theorem Th17: :: TOPGEN_4:17
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )
proof
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )
let F be Subset-Family of T; ::_thesis: ( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )
hereby ::_thesis: ( F is closed_for_countable_unions & F is compl-closed implies ( F is closed_for_countable_meets & F is compl-closed ) )
assume A1: ( F is closed_for_countable_meets & F is compl-closed ) ; ::_thesis: ( F is closed_for_countable_unions & F is 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; ::_thesis: ( G c= F implies union G in F )
assume A2: G c= F ; ::_thesis: union G in F
percases ( G = {} or G <> {} ) ;
suppose G = {} ; ::_thesis: union G in F
hence union G in F by A1, A2, Def5, SETFAM_1:1, ZFMISC_1:2; ::_thesis: verum
end;
suppose G <> {} ; ::_thesis: union G in F
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, Def5;
(meet (COMPLEMENT G9)) ` = ((union G9) `) ` by TOPS_2:6
.= union G9 ;
hence union G in F by A1, A3, PROB_1:def_1; ::_thesis: verum
end;
end;
end;
hence ( F is closed_for_countable_unions & F is compl-closed ) by A1, Def4; ::_thesis: verum
end;
assume A4: ( F is closed_for_countable_unions & F is compl-closed ) ; ::_thesis: ( F is closed_for_countable_meets & F is 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; ::_thesis: ( G c= F implies meet G in F )
assume A5: G c= F ; ::_thesis: meet G in F
percases ( G = {} or G <> {} ) ;
suppose G = {} ; ::_thesis: meet G in F
hence meet G in F by A4, A5, Def4, SETFAM_1:1, ZFMISC_1:2; ::_thesis: verum
end;
suppose G <> {} ; ::_thesis: meet G in F
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, Def4;
(union (COMPLEMENT G9)) ` = ((meet G9) `) ` by TOPS_2:7
.= meet G9 ;
hence meet G in F by A4, A6, PROB_1:def_1; ::_thesis: verum
end;
end;
end;
hence ( F is closed_for_countable_meets & F is compl-closed ) by A4, Def5; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster compl-closed all-open-containing closed_for_countable_unions -> all-closed-containing closed_for_countable_meets for Element of bool (bool the carrier of T);
coherence
for b1 being Subset-Family of T st b1 is all-open-containing & b1 is compl-closed & b1 is closed_for_countable_unions holds
( b1 is all-closed-containing & b1 is closed_for_countable_meets ) by Th14, Th17;
cluster compl-closed all-closed-containing closed_for_countable_meets -> all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);
coherence
for b1 being Subset-Family of T st b1 is all-closed-containing & b1 is compl-closed & b1 is closed_for_countable_meets holds
( b1 is all-open-containing & b1 is closed_for_countable_unions ) by Th14, Th17;
end;
begin
registration
let T be set ;
let F be countable Subset-Family of T;
cluster COMPLEMENT F -> countable ;
coherence
COMPLEMENT F is countable by Th1;
end;
registration
let T be TopSpace;
cluster empty -> open closed for Element of bool (bool the carrier of T);
coherence
for b1 being Subset-Family of T st b1 is empty holds
( b1 is open & b1 is closed )
proof
let F be Subset-Family of T; ::_thesis: ( F is empty implies ( F is open & F is closed ) )
assume F is empty ; ::_thesis: ( F is open & F is closed )
then ( ( for P being Subset of T st P in F holds
P is open ) & ( for P being Subset of T st P in F holds
P is closed ) ) ;
hence ( F is open & F is closed ) by TOPS_2:def_1, TOPS_2:def_2; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster countable open closed for Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( b1 is countable & b1 is open & b1 is closed )
proof
{} (bool the carrier of T) is open ;
hence ex b1 being Subset-Family of T st
( b1 is countable & b1 is open & b1 is closed ) ; ::_thesis: verum
end;
end;
theorem Th18: :: TOPGEN_4:18
for T being set holds {} is empty Subset-Family of T
proof
let T be set ; ::_thesis: {} is empty Subset-Family of T
{} (bool T) = {} ;
hence {} is empty Subset-Family of T ; ::_thesis: verum
end;
registration
cluster empty -> countable for set ;
coherence
for b1 being set st b1 is empty holds
b1 is countable ;
end;
begin
theorem Th19: :: TOPGEN_4:19
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
let F be Subset-Family of T; ::_thesis: ( F = {A} implies ( A is open iff F is open ) )
assume A1: F = {A} ; ::_thesis: ( A is open iff F is open )
hereby ::_thesis: ( F is open implies A is open )
assume A is open ; ::_thesis: F 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; ::_thesis: verum
end;
assume A2: F is open ; ::_thesis: A is open
A in F by A1, TARSKI:def_1;
hence A is open by A2, TOPS_2:def_1; ::_thesis: verum
end;
theorem Th20: :: TOPGEN_4:20
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
let F be Subset-Family of T; ::_thesis: ( F = {A} implies ( A is closed iff F is closed ) )
assume A1: F = {A} ; ::_thesis: ( A is closed iff F is closed )
hereby ::_thesis: ( F is closed implies A is closed )
assume A is closed ; ::_thesis: F 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; ::_thesis: verum
end;
assume A2: F is closed ; ::_thesis: A is closed
A in F by A1, TARSKI:def_1;
hence A is closed by A2, TOPS_2:def_2; ::_thesis: verum
end;
definition
let T be set ;
let F, G be Subset-Family of T;
:: original: INTERSECTION
redefine func INTERSECTION (F,G) -> Subset-Family of T;
coherence
INTERSECTION (F,G) is Subset-Family of T
proof
INTERSECTION (F,G) c= bool T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (F,G) or x in bool T )
assume x in INTERSECTION (F,G) ; ::_thesis: x in bool T
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 x in bool T ; ::_thesis: verum
end;
hence INTERSECTION (F,G) is Subset-Family of T ; ::_thesis: verum
end;
:: original: UNION
redefine func UNION (F,G) -> Subset-Family of T;
coherence
UNION (F,G) is Subset-Family of T
proof
UNION (F,G) c= bool T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION (F,G) or x in bool T )
assume x in UNION (F,G) ; ::_thesis: x in bool T
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 x in bool T by A4; ::_thesis: verum
end;
hence UNION (F,G) is Subset-Family of T ; ::_thesis: verum
end;
end;
theorem Th21: :: TOPGEN_4:21
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
INTERSECTION (F,G) is closed
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds
INTERSECTION (F,G) is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies INTERSECTION (F,G) is closed )
assume A1: ( F is closed & G is closed ) ; ::_thesis: INTERSECTION (F,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; ::_thesis: ( A in INTERSECTION (F,G) implies A is closed )
assume A in INTERSECTION (F,G) ; ::_thesis: A is closed
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 = X, Y = Y as Subset of T by A2;
( X is closed & Y is closed ) by A1, A2, TOPS_2:def_2;
hence A is closed by A3; ::_thesis: verum
end;
hence INTERSECTION (F,G) is closed by TOPS_2:def_2; ::_thesis: verum
end;
theorem Th22: :: TOPGEN_4:22
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
UNION (F,G) is closed
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds
UNION (F,G) is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies UNION (F,G) is closed )
assume A1: ( F is closed & G is closed ) ; ::_thesis: UNION (F,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; ::_thesis: ( A in UNION (F,G) implies A is closed )
assume A in UNION (F,G) ; ::_thesis: A is closed
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 = X, Y = Y as Subset of T by A2;
( X is closed & Y is closed ) by A1, A2, TOPS_2:def_2;
hence A is closed by A3; ::_thesis: verum
end;
hence UNION (F,G) is closed by TOPS_2:def_2; ::_thesis: verum
end;
theorem Th23: :: TOPGEN_4:23
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION (F,G) is open
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION (F,G) is open
let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies INTERSECTION (F,G) is open )
assume A1: ( F is open & G is open ) ; ::_thesis: INTERSECTION (F,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; ::_thesis: ( A in INTERSECTION (F,G) implies A is open )
assume A in INTERSECTION (F,G) ; ::_thesis: A is open
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 = X, Y = Y as Subset of T by A2;
( X is open & Y is open ) by A1, A2, TOPS_2:def_1;
hence A is open by A3; ::_thesis: verum
end;
hence INTERSECTION (F,G) is open by TOPS_2:def_1; ::_thesis: verum
end;
theorem Th24: :: TOPGEN_4:24
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
UNION (F,G) is open
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds
UNION (F,G) is open
let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies UNION (F,G) is open )
assume A1: ( F is open & G is open ) ; ::_thesis: UNION (F,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; ::_thesis: ( A in UNION (F,G) implies A is open )
assume A in UNION (F,G) ; ::_thesis: A is open
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 = X, Y = Y as Subset of T by A2;
( X is open & Y is open ) by A1, A2, TOPS_2:def_1;
hence A is open by A3; ::_thesis: verum
end;
hence UNION (F,G) is open by TOPS_2:def_1; ::_thesis: verum
end;
theorem Th25: :: TOPGEN_4:25
for T being set
for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]
proof
deffunc H1( set ) -> set = ($1 `1) /\ ($1 `2);
let T be set ; ::_thesis: for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]
let F, G be Subset-Family of T; ::_thesis: card (INTERSECTION (F,G)) c= card [:F,G:]
set XX = [:F,G:];
set IN = { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ;
set A = [:(bool T),(bool T):];
set AL = F;
set BL = G;
set C = INTERSECTION (F,G);
A1: { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } c= INTERSECTION (F,G)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } or a in INTERSECTION (F,G) )
assume a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ; ::_thesis: a in INTERSECTION (F,G)
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H1(X) and
A3: X in [:F,G:] ;
( X `1 in F & X `2 in G ) by A3, MCART_1:10;
hence a in INTERSECTION (F,G) by A2, SETFAM_1:def_5; ::_thesis: verum
end;
A4: INTERSECTION (F,G) c= { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in INTERSECTION (F,G) or a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } )
assume a in INTERSECTION (F,G) ; ::_thesis: a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
then consider X, Y being set such that
A5: ( X in F & Y in G ) and
A6: a = X /\ Y by SETFAM_1:def_5;
reconsider X = X, Y = Y as Subset of T by A5;
set XY = [X,Y];
A7: ( [X,Y] `1 = X & [X,Y] `2 = Y ) ;
[X,Y] in [:F,G:] by A5, ZFMISC_1:87;
hence a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } by A6, A7; ::_thesis: verum
end;
card { H1(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:] } c= card [:F,G:] from TREES_2:sch_2();
hence card (INTERSECTION (F,G)) c= card [:F,G:] by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th26: :: TOPGEN_4:26
for T being set
for F, G being Subset-Family of T holds card (UNION (F,G)) c= card [:F,G:]
proof
deffunc H1( set ) -> set = ($1 `1) \/ ($1 `2);
let T be set ; ::_thesis: for F, G being Subset-Family of T holds card (UNION (F,G)) c= card [:F,G:]
let F, G be Subset-Family of T; ::_thesis: card (UNION (F,G)) c= card [:F,G:]
set XX = [:F,G:];
set IN = { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ;
set A = [:(bool T),(bool T):];
set AL = F;
set BL = G;
set C = UNION (F,G);
A1: { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } = UNION (F,G)
proof
thus { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } c= UNION (F,G) :: according to XBOOLE_0:def_10 ::_thesis: UNION (F,G) c= { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } or a in UNION (F,G) )
assume a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } ; ::_thesis: a in UNION (F,G)
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H1(X) and
A3: X in [:F,G:] ;
( X `1 in F & X `2 in G ) by A3, MCART_1:10;
hence a in UNION (F,G) by A2, SETFAM_1:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in UNION (F,G) or a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } )
assume a in UNION (F,G) ; ::_thesis: a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] }
then consider X, Y being set such that
A4: ( X in F & Y in G ) and
A5: a = X \/ Y by SETFAM_1:def_4;
reconsider X = X, Y = Y as Subset of T by A4;
set XY = [X,Y];
A6: ( [X,Y] `1 = X & [X,Y] `2 = Y ) ;
[X,Y] in [:F,G:] by A4, ZFMISC_1:87;
hence a in { H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:] } by A5, A6; ::_thesis: verum
end;
card { H1(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:] } c= card [:F,G:] from TREES_2:sch_2();
hence card (UNION (F,G)) c= card [:F,G:] by A1; ::_thesis: verum
end;
theorem Th27: :: TOPGEN_4:27
for F, G being set holds union (UNION (F,G)) c= (union F) \/ (union G)
proof
let F, G be set ; ::_thesis: union (UNION (F,G)) c= (union F) \/ (union G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (UNION (F,G)) or x in (union F) \/ (union G) )
assume x in union (UNION (F,G)) ; ::_thesis: x in (union F) \/ (union 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;
percases ( x in f or x in g ) by A1, A5, XBOOLE_0:def_3;
suppose x in f ; ::_thesis: x in (union F) \/ (union G)
then x in union F by A3, TARSKI:def_4;
hence x in (union F) \/ (union G) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in g ; ::_thesis: x in (union F) \/ (union G)
then x in union G by A4, TARSKI:def_4;
hence x in (union F) \/ (union G) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem Th28: :: TOPGEN_4:28
for F, G being set st F <> {} & G <> {} holds
(union F) \/ (union G) = union (UNION (F,G))
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies (union F) \/ (union G) = union (UNION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; ::_thesis: (union F) \/ (union G) = union (UNION (F,G))
thus (union F) \/ (union G) c= union (UNION (F,G)) :: according to XBOOLE_0:def_10 ::_thesis: union (UNION (F,G)) c= (union F) \/ (union G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union F) \/ (union G) or x in union (UNION (F,G)) )
assume A3: x in (union F) \/ (union G) ; ::_thesis: x in union (UNION (F,G))
percases ( x in union F or x in union G ) by A3, XBOOLE_0:def_3;
supposeA4: x in union F ; ::_thesis: x in union (UNION (F,G))
consider W being set 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;
set YW = Y \/ W;
( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by A7, A5, SETFAM_1:def_4, XBOOLE_1:7;
hence x in union (UNION (F,G)) by A6, TARSKI:def_4; ::_thesis: verum
end;
supposeA8: x in union G ; ::_thesis: x in union (UNION (F,G))
consider W being set 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;
set YW = W \/ Y;
( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by A11, A9, SETFAM_1:def_4, XBOOLE_1:7;
hence x in union (UNION (F,G)) by A10, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
thus union (UNION (F,G)) c= (union F) \/ (union G) by Th27; ::_thesis: verum
end;
theorem Th29: :: TOPGEN_4:29
for F being set holds UNION ({},F) = {}
proof
let F be set ; ::_thesis: UNION ({},F) = {}
UNION ({},F) c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION ({},F) or x in {} )
assume x in UNION ({},F) ; ::_thesis: x in {}
then ex x1, x2 being set st
( x1 in {} & x2 in F & x = x1 \/ x2 ) by SETFAM_1:def_4;
hence x in {} ; ::_thesis: verum
end;
hence UNION ({},F) = {} ; ::_thesis: verum
end;
theorem :: TOPGEN_4:30
for F, G being set holds
( not UNION (F,G) = {} or F = {} or G = {} )
proof
let F, G be set ; ::_thesis: ( not UNION (F,G) = {} or F = {} or G = {} )
assume A1: UNION (F,G) = {} ; ::_thesis: ( F = {} or G = {} )
assume that
A2: F <> {} and
A3: G <> {} ; ::_thesis: contradiction
consider X being set such that
A4: X in F by A2, XBOOLE_0:def_1;
consider Y being set such that
A5: Y in G by A3, XBOOLE_0:def_1;
X \/ Y in UNION (F,G) by A4, A5, SETFAM_1:def_4;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: TOPGEN_4:31
for F, G being set holds
( not INTERSECTION (F,G) = {} or F = {} or G = {} )
proof
let F, G be set ; ::_thesis: ( not INTERSECTION (F,G) = {} or F = {} or G = {} )
assume that
A1: INTERSECTION (F,G) = {} and
A2: F <> {} and
A3: G <> {} ; ::_thesis: contradiction
consider X being set such that
A4: X in F by A2, XBOOLE_0:def_1;
consider Y being set such that
A5: Y in G by A3, XBOOLE_0:def_1;
X /\ Y in INTERSECTION (F,G) by A4, A5, SETFAM_1:def_5;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th32: :: TOPGEN_4:32
for F, G being set holds meet (UNION (F,G)) c= (meet F) \/ (meet G)
proof
let F, G be set ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA1: ( F <> {} & G <> {} ) ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (UNION (F,G)) or x in (meet F) \/ (meet G) )
assume A2: x in meet (UNION (F,G)) ; ::_thesis: x in (meet F) \/ (meet G)
assume A3: not x in (meet F) \/ (meet G) ; ::_thesis: contradiction
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 contradiction by A2, SETFAM_1:def_1; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
then UNION (F,G) = {} by Th29;
then meet (UNION (F,G)) = {} by SETFAM_1:def_1;
hence meet (UNION (F,G)) c= (meet F) \/ (meet G) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:33
for F, G being set st F <> {} & G <> {} holds
meet (UNION (F,G)) = (meet F) \/ (meet G)
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies meet (UNION (F,G)) = (meet F) \/ (meet G) )
assume A1: ( F <> {} & G <> {} ) ; ::_thesis: meet (UNION (F,G)) = (meet F) \/ (meet G)
thus meet (UNION (F,G)) c= (meet F) \/ (meet G) by Th32; :: according to XBOOLE_0:def_10 ::_thesis: (meet F) \/ (meet G) c= meet (UNION (F,G))
thus (meet F) \/ (meet G) c= meet (UNION (F,G)) by A1, SETFAM_1:29; ::_thesis: verum
end;
theorem Th34: :: TOPGEN_4:34
for F, G being set st F <> {} & G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; ::_thesis: (meet F) /\ (meet G) = meet (INTERSECTION (F,G))
consider y being set such that
A3: y in F by A1, XBOOLE_0:def_1;
consider z being set such that
A4: z in G by A2, XBOOLE_0:def_1;
A5: meet (INTERSECTION (F,G)) c= (meet F) /\ (meet G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (INTERSECTION (F,G)) or x in (meet F) /\ (meet G) )
assume A6: x in meet (INTERSECTION (F,G)) ; ::_thesis: x in (meet F) /\ (meet G)
for Z being set st Z in G holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in G implies x in Z )
assume Z in G ; ::_thesis: x in Z
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 x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then A7: x in meet G by A2, SETFAM_1:def_1;
for Z being set st Z in F holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in F implies x in Z )
assume Z in F ; ::_thesis: x in Z
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 x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then x in meet F by A1, SETFAM_1:def_1;
hence x in (meet F) /\ (meet G) by A7, XBOOLE_0:def_4; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet F) /\ (meet G) or x in meet (INTERSECTION (F,G)) )
assume x in (meet F) /\ (meet G) ; ::_thesis: x in meet (INTERSECTION (F,G))
then A9: ( x in meet F & x in meet G ) by XBOOLE_0:def_4;
for Z being set st Z in INTERSECTION (F,G) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in INTERSECTION (F,G) implies x in Z )
assume Z in INTERSECTION (F,G) ; ::_thesis: x in Z
then consider Z1, Z2 being 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 x in Z by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence x in meet (INTERSECTION (F,G)) by A8, SETFAM_1:def_1; ::_thesis: verum
end;
hence (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let T be TopSpace;
let A be Subset of T;
attrA is F_sigma means :Def6: :: TOPGEN_4:def 6
ex F being countable closed Subset-Family of T st A = union F;
end;
:: deftheorem Def6 defines F_sigma TOPGEN_4:def_6_:_
for T being TopSpace
for A being Subset of T holds
( A is F_sigma iff ex F being countable closed Subset-Family of T st A = union F );
definition
let T be TopSpace;
let A be Subset of T;
attrA is G_delta means :Def7: :: TOPGEN_4:def 7
ex F being countable open Subset-Family of T st A = meet F;
end;
:: deftheorem Def7 defines G_delta TOPGEN_4:def_7_:_
for T being TopSpace
for A being Subset of T holds
( A is G_delta iff ex F being countable open Subset-Family of T st A = meet F );
registration
let T be non empty TopSpace;
cluster empty -> F_sigma G_delta for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
( b1 is F_sigma & b1 is G_delta )
proof
let S be Subset of T; ::_thesis: ( S is empty implies ( S is F_sigma & S is G_delta ) )
assume S is empty ; ::_thesis: ( S is F_sigma & S is G_delta )
then A1: S = {} T ;
thus S is F_sigma ::_thesis: S is G_delta
proof
reconsider E = {} as empty Subset-Family of T by Th18;
{} T = union E by ZFMISC_1:2;
hence S is F_sigma by Def6, A1; ::_thesis: verum
end;
reconsider F = {({} T)} as Subset-Family of T ;
( F is open & {} T = meet F ) by Th19, SETFAM_1:10;
hence S is G_delta by Def7, A1; ::_thesis: verum
end;
end;
theorem Th35: :: TOPGEN_4:35
for T being non empty TopSpace holds [#] T is F_sigma
proof
let T be non empty TopSpace; ::_thesis: [#] T is F_sigma
reconsider F = {([#] T)} as Subset-Family of T ;
( F is closed & [#] T = union F ) by Th20, ZFMISC_1:25;
hence [#] T is F_sigma by Def6; ::_thesis: verum
end;
theorem Th36: :: TOPGEN_4:36
for T being non empty TopSpace holds [#] T is G_delta
proof
let T be non empty TopSpace; ::_thesis: [#] T is G_delta
reconsider F = {([#] T)} as Subset-Family of T ;
( F is open & [#] T = meet F ) by Th19, SETFAM_1:10;
hence [#] T is G_delta by Def7; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster [#] T -> F_sigma G_delta ;
coherence
( [#] T is F_sigma & [#] T is G_delta ) by Th35, Th36;
end;
theorem :: TOPGEN_4:37
for T being non empty TopSpace
for A being Subset of T st A is F_sigma holds
A ` is G_delta
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is F_sigma holds
A ` is G_delta
let A be Subset of T; ::_thesis: ( A is F_sigma implies A ` is G_delta )
assume A is F_sigma ; ::_thesis: A ` is G_delta
then consider F being countable closed Subset-Family of T such that
A1: A = union F by Def6;
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: A ` is G_delta
set G = COMPLEMENT F;
A3: COMPLEMENT F is open by TOPS_2:9;
(union F) ` = meet (COMPLEMENT F) by A2, TOPS_2:6;
hence A ` is G_delta by A1, A3, Def7; ::_thesis: verum
end;
suppose F = {} ; ::_thesis: A ` is G_delta
then A ` = [#] T by A1, ZFMISC_1:2;
hence A ` is G_delta ; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:38
for T being non empty TopSpace
for A being Subset of T st A is G_delta holds
A ` is F_sigma
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is G_delta holds
A ` is F_sigma
let A be Subset of T; ::_thesis: ( A is G_delta implies A ` is F_sigma )
assume A is G_delta ; ::_thesis: A ` is F_sigma
then consider F being countable open Subset-Family of T such that
A1: A = meet F by Def7;
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: A ` is F_sigma
set G = COMPLEMENT F;
A3: COMPLEMENT F is closed by TOPS_2:10;
(meet F) ` = union (COMPLEMENT F) by A2, TOPS_2:7;
hence A ` is F_sigma by A1, A3, Def6; ::_thesis: verum
end;
suppose F = {} ; ::_thesis: A ` is F_sigma
then A ` = [#] T by A1, SETFAM_1:1;
hence A ` is F_sigma ; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:39
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A /\ B is F_sigma
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A /\ B is F_sigma
let A, B be Subset of T; ::_thesis: ( A is F_sigma & B is F_sigma implies A /\ B is F_sigma )
assume that
A1: A is F_sigma and
A2: B is F_sigma ; ::_thesis: A /\ B is F_sigma
consider F being countable closed Subset-Family of T such that
A3: A = union F by A1, Def6;
consider G being countable closed Subset-Family of T such that
A4: B = union G by A2, Def6;
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 A /\ B is F_sigma by A5, A6, Def6; ::_thesis: verum
end;
theorem :: TOPGEN_4:40
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A \/ B is F_sigma
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A \/ B is F_sigma
let A, B be Subset of T; ::_thesis: ( A is F_sigma & B is F_sigma implies A \/ B is F_sigma )
assume that
A1: A is F_sigma and
A2: B is F_sigma ; ::_thesis: A \/ B is F_sigma
consider F being countable closed Subset-Family of T such that
A3: A = union F by A1, Def6;
consider G being countable closed Subset-Family of T such that
A4: B = union G by A2, Def6;
reconsider H = UNION (F,G) as Subset-Family of T ;
percases ( ( A <> {} & B <> {} ) or A = {} or B = {} ) ;
supposeA5: ( A <> {} & B <> {} ) ; ::_thesis: A \/ B is F_sigma
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 A \/ B is F_sigma by A6, A7, Def6; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: A \/ B is F_sigma
hence A \/ B is F_sigma by A2; ::_thesis: verum
end;
suppose B = {} ; ::_thesis: A \/ B is F_sigma
hence A \/ B is F_sigma by A1; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:41
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta
let A, B be Subset of T; ::_thesis: ( A is G_delta & B is G_delta implies A \/ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; ::_thesis: A \/ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1, Def7;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2, Def7;
reconsider H = UNION (F,G) as Subset-Family of T ;
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA5: ( F <> {} & G <> {} ) ; ::_thesis: A \/ B is G_delta
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, XBOOLE_0:def_10;
( 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 A \/ B is G_delta by A7, A8, Def7; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: A \/ B is G_delta
then ( A = {} or B = {} ) by A3, A4, SETFAM_1:def_1;
hence A \/ B is G_delta by A1, A2; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:42
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta
let A, B be Subset of T; ::_thesis: ( A is G_delta & B is G_delta implies A /\ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; ::_thesis: A /\ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1, Def7;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2, Def7;
reconsider H = INTERSECTION (F,G) as Subset-Family of T ;
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA5: ( F <> {} & G <> {} ) ; ::_thesis: A /\ B is G_delta
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 A /\ B is G_delta by A6, A7, Def7; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: A /\ B is G_delta
then ( A = {} or B = {} ) by A3, A4, SETFAM_1:def_1;
then A /\ B = {} T ;
hence A /\ B is G_delta ; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_4:43
for T being non empty TopSpace
for A being Subset of T st A is closed holds
A is F_sigma
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is closed holds
A is F_sigma
let A be Subset of T; ::_thesis: ( A is closed implies A is F_sigma )
assume A is closed ; ::_thesis: A is F_sigma
then reconsider F = {A} as countable closed Subset-Family of T by Th20;
take F ; :: according to TOPGEN_4:def_6 ::_thesis: A = union F
thus A = union F by ZFMISC_1:25; ::_thesis: verum
end;
theorem :: TOPGEN_4:44
for T being non empty TopSpace
for A being Subset of T st A is open holds
A is G_delta
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is open holds
A is G_delta
let A be Subset of T; ::_thesis: ( A is open implies A is G_delta )
assume A is open ; ::_thesis: A is G_delta
then reconsider F = {A} as countable open Subset-Family of T by Th19;
take F ; :: according to TOPGEN_4:def_7 ::_thesis: A = meet F
thus A = meet F by SETFAM_1:10; ::_thesis: verum
end;
theorem :: TOPGEN_4:45
for A being Subset of R^1 st A = RAT holds
A is F_sigma
proof
defpred S1[ set ] means ex a being Element of RAT st a = $1;
defpred S2[ set ] means ex a being Element of RAT st {a} = $1;
let A be Subset of R^1; ::_thesis: ( A = RAT implies A is F_sigma )
ex F being set st
for x being set holds
( x in F iff ( x in bool RAT & S2[x] ) ) from XBOOLE_0:sch_1();
then consider F being set such that
A1: for x being set holds
( x in F iff ( x in bool RAT & S2[x] ) ) ;
A2: bool RAT c= bool REAL by NUMBERS:12, ZFMISC_1:67;
F c= bool the carrier of R^1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in bool the carrier of R^1 )
assume x in F ; ::_thesis: x in bool the carrier of R^1
then x in bool RAT by A1;
hence x in bool the carrier of R^1 by A2, TOPMETR:17; ::_thesis: verum
end;
then reconsider F = F as Subset-Family of R^1 ;
assume A3: A = RAT ; ::_thesis: A is F_sigma
ex F being Subset-Family of R^1 st
( F is closed & F is countable & A = union F )
proof
take F ; ::_thesis: ( F is closed & F is countable & A = union F )
for B being Subset of R^1 st B in F holds
B is closed
proof
let B be Subset of R^1; ::_thesis: ( B in F implies B is closed )
assume B in F ; ::_thesis: B is closed
then ex a being Element of RAT st {a} = B by A1;
hence B is closed ; ::_thesis: verum
end;
hence F is closed by TOPS_2:def_2; ::_thesis: ( F is countable & A = union F )
A4: F = { {x} where x is Element of RAT : S1[x] }
proof
thus F c= { {x} where x is Element of RAT : S1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { {x} where x is Element of RAT : S1[x] } c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F or y in { {x} where x is Element of RAT : S1[x] } )
assume y in F ; ::_thesis: y in { {x} where x is Element of RAT : S1[x] }
then S2[y] by A1;
hence y in { {x} where x is Element of RAT : S1[x] } ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { {x} where x is Element of RAT : S1[x] } or y in F )
assume y in { {x} where x is Element of RAT : S1[x] } ; ::_thesis: y in F
then ex z being Element of RAT st
( y = {z} & S1[z] ) ;
hence y in F by A1; ::_thesis: verum
end;
{ {x} where x is Element of RAT : S1[x] } is countable from TOPGEN_4:sch_1();
hence F is countable by A4; ::_thesis: A = union F
thus A c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union F )
assume x in A ; ::_thesis: x in union F
then reconsider x = x as Element of RAT by A3;
( {x} in F & x in {x} ) by A1, TARSKI:def_1;
hence x in union F by TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in A )
assume x in union F ; ::_thesis: x in A
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 x in A by A3, A5; ::_thesis: verum
end;
hence A is F_sigma by Def6; ::_thesis: verum
end;
begin
definition
let T be TopSpace;
attrT is T_1/2 means :Def8: :: TOPGEN_4:def 8
for A being Subset of T holds Der A is closed ;
end;
:: deftheorem Def8 defines T_1/2 TOPGEN_4:def_8_:_
for T being TopSpace holds
( T is T_1/2 iff for A being Subset of T holds Der A is closed );
theorem Th46: :: TOPGEN_4:46
for T being TopSpace st T is T_1 holds
T is T_1/2
proof
let T be TopSpace; ::_thesis: ( T is T_1 implies T is T_1/2 )
assume A1: T is T_1 ; ::_thesis: T is T_1/2
for A being Subset of T holds Der A is closed
proof
let A be Subset of T; ::_thesis: Der A is closed
Der A = Cl (Der A) by A1, TOPGEN_1:33;
hence Der A is closed ; ::_thesis: verum
end;
hence T is T_1/2 by Def8; ::_thesis: verum
end;
theorem Th47: :: TOPGEN_4:47
for T being non empty TopSpace st T is T_1/2 holds
T is T_0
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1/2 implies T is T_0 )
assume A1: T is T_1/2 ; ::_thesis: T is T_0
now__::_thesis:_for_x,_y_being_Point_of_T_st_x_<>_y_&_x_in_Cl_{y}_holds_
not_y_in_Cl_{x}
let x, y be Point of T; ::_thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )
assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} )
assume that
A3: x in Cl {y} and
A4: y in Cl {x} ; ::_thesis: contradiction
ex G being Subset of T st
( G is open & y in G & not {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= the a_neighborhood of x and
A6: x in V by CONNSP_2:6;
assume x in Der {x} ; ::_thesis: contradiction
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 contradiction by A8, TARSKI:def_1; ::_thesis: verum
end;
then A9: x in (Der {x}) ` by SUBSET_1:29;
assume A10: for G being Subset of T st G is open & y in G holds
{x} meets G ; ::_thesis: contradiction
for U being open Subset of T st y in U holds
ex r being Point of T st
( r in {x} /\ U & y <> r )
proof
let U be open Subset of T; ::_thesis: ( y in U implies ex r being Point of T st
( r in {x} /\ U & y <> r ) )
assume y in U ; ::_thesis: ex r being Point of T st
( r in {x} /\ U & y <> r )
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 ex r being Point of T st
( r in {x} /\ U & y <> r ) by A2; ::_thesis: verum
end;
then y in Der {x} by TOPGEN_1:17;
then A12: not y in (Der {x}) ` by XBOOLE_0:def_5;
Der {x} is closed by A1, Def8;
then {y} meets (Der {x}) ` by A3, A9, PRE_TOPC:24;
hence contradiction by A12, ZFMISC_1:50; ::_thesis: verum
end;
hence contradiction by A4, PRE_TOPC:24; ::_thesis: verum
end;
hence T is T_0 by TSP_1:def_6; ::_thesis: verum
end;
registration
cluster TopSpace-like T_1/2 -> T_0 for TopStruct ;
coherence
for b1 being TopSpace st b1 is T_1/2 holds
b1 is T_0
proof
let T be TopSpace; ::_thesis: ( T is T_1/2 implies T is T_0 )
percases ( not T is empty or T is empty ) ;
suppose not T is empty ; ::_thesis: ( T is T_1/2 implies T is T_0 )
then reconsider T9 = T as non empty TopSpace ;
assume T is T_1/2 ; ::_thesis: T is T_0
then T9 is T_1/2 ;
hence T is T_0 by Th47; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: ( T is T_1/2 implies T is T_0 )
then reconsider T9 = T as empty TopSpace ;
T9 is T_0 ;
hence ( T is T_1/2 implies T is T_0 ) ; ::_thesis: verum
end;
end;
end;
cluster TopSpace-like T_1 -> T_1/2 for TopStruct ;
coherence
for b1 being TopSpace st b1 is T_1 holds
b1 is T_1/2 by Th46;
end;
begin
definition
let T be non empty TopSpace;
let A be Subset of T;
let x be Point of T;
predx is_a_condensation_point_of A means :Def9: :: TOPGEN_4:def 9
for N being a_neighborhood of x holds not N /\ A is countable ;
end;
:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def_9_:_
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x is_a_condensation_point_of A iff for N being a_neighborhood of x holds not N /\ A is countable );
theorem Th48: :: TOPGEN_4:48
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T st x is_a_condensation_point_of A & A c= B holds
x is_a_condensation_point_of B
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for x being Point of T st x is_a_condensation_point_of A & A c= B holds
x is_a_condensation_point_of B
let A, B be Subset of T; ::_thesis: for x being Point of T st x is_a_condensation_point_of A & A c= B holds
x is_a_condensation_point_of B
let x be Point of T; ::_thesis: ( x is_a_condensation_point_of A & A c= B implies x is_a_condensation_point_of B )
assume that
A1: x is_a_condensation_point_of A and
A2: A c= B ; ::_thesis: x is_a_condensation_point_of B
for N being a_neighborhood of x holds not N /\ B is countable
proof
let N be a_neighborhood of x; ::_thesis: not N /\ B is countable
N /\ A c= N /\ B by A2, XBOOLE_1:26;
hence not N /\ B is countable by A1, Def9; ::_thesis: verum
end;
hence x is_a_condensation_point_of B by Def9; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
let A be Subset of T;
funcA ^0 -> Subset of T means :Def10: :: TOPGEN_4:def 10
for x being Point of T holds
( x in it iff x is_a_condensation_point_of A );
existence
ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
hence ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds
( x in b2 iff x is_a_condensation_point_of A ) ) holds
b1 = b2
proof
defpred S1[ Point of T] means $1 is_a_condensation_point_of A;
let A1, A2 be Subset of T; ::_thesis: ( ( for x being Point of T holds
( x in A1 iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds
( x in A2 iff x is_a_condensation_point_of A ) ) implies A1 = A2 )
assume that
A1: for x being Element of T holds
( x in A1 iff S1[x] ) and
A2: for x being Element of T holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
thus A1 = A2 from SUBSET_1:sch_2(A1, A2); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines ^0 TOPGEN_4:def_10_:_
for T being non empty TopSpace
for A, b3 being Subset of T holds
( b3 = A ^0 iff for x being Point of T holds
( x in b3 iff x is_a_condensation_point_of A ) );
theorem Th49: :: TOPGEN_4:49
for T being non empty TopSpace
for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
let A be Subset of T; ::_thesis: for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
let p be Point of T; ::_thesis: ( p is_a_condensation_point_of A implies p is_an_accumulation_point_of A )
assume A1: p is_a_condensation_point_of A ; ::_thesis: p is_an_accumulation_point_of A
for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U )
proof
let U be open Subset of T; ::_thesis: ( p in U implies ex q being Point of T st
( q <> p & q in A & q in U ) )
assume p in U ; ::_thesis: ex q being Point of T st
( q <> p & q in A & q 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, Def9;
consider q being Element of NU such that
A2: p <> q by BORSUK_4:2;
q in NU ;
then reconsider q = q as Point of T ;
( q in A & q in U ) by XBOOLE_0:def_4;
hence ex q being Point of T st
( q <> p & q in A & q in U ) by A2; ::_thesis: verum
end;
hence p is_an_accumulation_point_of A by TOPGEN_1:21; ::_thesis: verum
end;
theorem :: TOPGEN_4:50
for T being non empty TopSpace
for A being Subset of T holds A ^0 c= Der A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds A ^0 c= Der A
let A be Subset of T; ::_thesis: A ^0 c= Der A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^0 or x in Der A )
assume A1: x in A ^0 ; ::_thesis: x in Der A
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 x in Der A by TOPGEN_1:16; ::_thesis: verum
end;
theorem :: TOPGEN_4:51
for T being non empty TopSpace
for A being Subset of T holds A ^0 = Cl (A ^0)
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds A ^0 = Cl (A ^0)
let A be Subset of T; ::_thesis: A ^0 = Cl (A ^0)
thus A ^0 c= Cl (A ^0) by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl (A ^0) c= A ^0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (A ^0) or x in A ^0 )
assume A1: x in Cl (A ^0) ; ::_thesis: x in A ^0
then reconsider p = x as Point of T ;
for N being a_neighborhood of p holds not N /\ A is countable
proof
let N be a_neighborhood of p; ::_thesis: not N /\ A is countable
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 set 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 = 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 not N /\ A is countable by A7, Def9; ::_thesis: verum
end;
then p is_a_condensation_point_of A by Def9;
hence x in A ^0 by Def10; ::_thesis: verum
end;
theorem Th52: :: TOPGEN_4:52
for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
A ^0 c= B ^0
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A c= B holds
A ^0 c= B ^0
let A, B be Subset of T; ::_thesis: ( A c= B implies A ^0 c= B ^0 )
assume A1: A c= B ; ::_thesis: A ^0 c= B ^0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^0 or x in B ^0 )
assume A2: x in A ^0 ; ::_thesis: x in B ^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 x in B ^0 by Def10; ::_thesis: verum
end;
theorem Th53: :: TOPGEN_4:53
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
let A, B be Subset of T; ::_thesis: for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
let x be Point of T; ::_thesis: ( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
assume A1: x is_a_condensation_point_of A \/ B ; ::_thesis: ( x is_a_condensation_point_of A or x is_a_condensation_point_of B )
assume that
A2: not x is_a_condensation_point_of A and
A3: not x is_a_condensation_point_of B ; ::_thesis: contradiction
consider N1 being a_neighborhood of x such that
A4: N1 /\ A is countable by A2, Def9;
consider N2 being a_neighborhood of x such that
A5: N2 /\ B is countable by A3, Def9;
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, XBOOLE_1: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 contradiction by A1, Def9; ::_thesis: verum
end;
theorem :: TOPGEN_4:54
for T being non empty TopSpace
for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)
let A, B be Subset of T; ::_thesis: (A \/ B) ^0 = (A ^0) \/ (B ^0)
thus (A \/ B) ^0 c= (A ^0) \/ (B ^0) :: according to XBOOLE_0:def_10 ::_thesis: (A ^0) \/ (B ^0) c= (A \/ B) ^0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) ^0 or x in (A ^0) \/ (B ^0) )
assume A1: x in (A \/ B) ^0 ; ::_thesis: x in (A ^0) \/ (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 x in (A ^0) \/ (B ^0) by XBOOLE_0:def_3; ::_thesis: verum
end;
( A ^0 c= (A \/ B) ^0 & B ^0 c= (A \/ B) ^0 ) by Th52, XBOOLE_1:7;
hence (A ^0) \/ (B ^0) c= (A \/ B) ^0 by XBOOLE_1:8; ::_thesis: verum
end;
theorem Th55: :: TOPGEN_4:55
for T being non empty TopSpace
for A being Subset of T st A is countable holds
for x being Point of T holds not x is_a_condensation_point_of A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is countable holds
for x being Point of T holds not x is_a_condensation_point_of A
let A be Subset of T; ::_thesis: ( A is countable implies for x being Point of T holds not x is_a_condensation_point_of A )
assume A1: A is countable ; ::_thesis: for x being Point of T holds not x is_a_condensation_point_of A
given x being Point of T such that A2: x is_a_condensation_point_of A ; ::_thesis: contradiction
set N = the a_neighborhood of x;
not the a_neighborhood of x /\ A is countable by A2, Def9;
hence contradiction by A1, CARD_3:94; ::_thesis: verum
end;
theorem Th56: :: TOPGEN_4:56
for T being non empty TopSpace
for A being Subset of T st A is countable holds
A ^0 = {}
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is countable holds
A ^0 = {}
let A be Subset of T; ::_thesis: ( A is countable implies A ^0 = {} )
assume A1: A is countable ; ::_thesis: A ^0 = {}
assume A ^0 <> {} ; ::_thesis: contradiction
then consider x being set 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 contradiction by A1, Th55; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let A be countable Subset of T;
clusterA ^0 -> empty ;
coherence
A ^0 is empty by Th56;
end;
theorem :: TOPGEN_4:57
for T being non empty TopSpace st T is second-countable holds
ex B being Basis of T st B is countable
proof
let T be non empty TopSpace; ::_thesis: ( T is second-countable implies ex B being Basis of T st B is countable )
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
assume T is second-countable ; ::_thesis: ex B being Basis of T st B is countable
then card B1 c= omega by A1, WAYBEL23:def_6;
then card (card B1) c= card omega by CARD_1:11;
then B1 is countable by WAYBEL12:1;
hence ex B being Basis of T st B is countable ; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like second-countable for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is second-countable & not b1 is empty )
proof
set T = the non empty finite TopSpace;
take the non empty finite TopSpace ; ::_thesis: ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty )
thus ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty ) ; ::_thesis: verum
end;
end;
begin
registration
let T be non empty TopSpace;
cluster TotFam T -> non empty compl-closed all-open-containing closed_for_countable_unions ;
coherence
( not TotFam T is empty & TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
proof
thus not TotFam T is empty ; ::_thesis: ( TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
thus TotFam T is all-open-containing ::_thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
proof
let A be Subset of T; :: according to TOPGEN_4:def_2 ::_thesis: ( A is open implies A in TotFam T )
assume A is open ; ::_thesis: A in TotFam T
thus A in TotFam T ; ::_thesis: verum
end;
for A being Subset of T st A in TotFam T holds
A ` in TotFam T ;
hence TotFam T is compl-closed by PROB_1:def_1; ::_thesis: TotFam T is closed_for_countable_unions
for G being countable Subset-Family of T st G c= TotFam T holds
union G in TotFam T ;
hence TotFam T is closed_for_countable_unions by Def4; ::_thesis: verum
end;
end;
theorem :: TOPGEN_4:58
for T being set
for A being SetSequence of T holds rng A is non empty countable Subset-Family of T
proof
let T be set ; ::_thesis: for A being SetSequence of T holds rng A is non empty countable Subset-Family of T
let A be SetSequence of T; ::_thesis: rng A is non empty countable Subset-Family 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 rng A is non empty countable Subset-Family of T ; ::_thesis: verum
end;
theorem Th59: :: TOPGEN_4:59
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing
let F, G be Subset-Family of T; ::_thesis: ( F is all-open-containing & F c= G implies G is all-open-containing )
assume that
A1: F is all-open-containing and
A2: F c= G ; ::_thesis: G is all-open-containing
for A being Subset of T st A is open holds
A in G
proof
let A be Subset of T; ::_thesis: ( A is open implies A in G )
assume A is open ; ::_thesis: A in G
then A in F by A1, Def2;
hence A in G by A2; ::_thesis: verum
end;
hence G is all-open-containing by Def2; ::_thesis: verum
end;
theorem :: TOPGEN_4:60
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing
proof
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing
let F, G be Subset-Family of T; ::_thesis: ( F is all-closed-containing & F c= G implies G is all-closed-containing )
assume that
A1: F is all-closed-containing and
A2: F c= G ; ::_thesis: G is all-closed-containing
for A being Subset of T st A is closed holds
A in G
proof
let A be Subset of T; ::_thesis: ( A is closed implies A in G )
assume A is closed ; ::_thesis: A in G
then A in F by A1, Def3;
hence A in G by A2; ::_thesis: verum
end;
hence G is all-closed-containing by Def3; ::_thesis: verum
end;
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 all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets for Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( b1 is compl-closed & b1 is closed_for_countable_unions & b1 is closed_for_countable_meets & b1 is all-closed-containing & b1 is all-open-containing )
proof
take TotFam T ; ::_thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing )
thus ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing ) ; ::_thesis: verum
end;
end;
theorem Th61: :: TOPGEN_4:61
for T being non empty TopSpace holds
( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
proof
let T be non empty TopSpace; ::_thesis: ( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
set E = sigma (TotFam T);
TotFam T c= sigma (TotFam T) by PROB_1:def_9;
hence sigma (TotFam T) is all-open-containing by Th59; ::_thesis: ( sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
thus sigma (TotFam T) is compl-closed ; ::_thesis: sigma (TotFam T) is closed_for_countable_unions
thus sigma (TotFam T) is closed_for_countable_unions ; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster sigma (TotFam T) -> all-open-containing closed_for_countable_unions ;
coherence
( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions ) by Th61;
end;
registration
let T be non empty 1-sorted ;
cluster non empty compl-closed sigma-additive closed_for_countable_unions for Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( b1 is sigma-additive & b1 is compl-closed & b1 is closed_for_countable_unions & not b1 is empty )
proof
take sigma (TotFam T) ; ::_thesis: ( sigma (TotFam T) is sigma-additive & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions & not sigma (TotFam T) is empty )
thus ( sigma (TotFam T) is sigma-additive & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions & not sigma (TotFam T) is empty ) ; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions for Element of bool (bool the carrier of T);
coherence
for b1 being SigmaField of T holds b1 is closed_for_countable_unions ;
end;
theorem :: TOPGEN_4:62
for T being non empty TopSpace
for F being Subset-Family of T st F is compl-closed & F is closed_for_countable_unions holds
F is SigmaField of T by Th13;
registration
let T be non empty TopSpace;
cluster non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);
existence
ex b1 being SigmaField of T st b1 is all-open-containing
proof
take sigma (TotFam T) ; ::_thesis: sigma (TotFam T) is all-open-containing
thus sigma (TotFam T) is all-open-containing ; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
cluster Topology_of T -> open all-open-containing ;
coherence
( Topology_of T is open & Topology_of T is all-open-containing )
proof
set E = Topology_of T;
thus Topology_of T is open ; ::_thesis: Topology_of T is all-open-containing
Topology_of T is all-open-containing
proof
let A be Subset of T; :: according to TOPGEN_4:def_2 ::_thesis: ( A is open implies A in Topology_of T )
assume A is open ; ::_thesis: A in Topology_of T
hence A in Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence Topology_of T is all-open-containing ; ::_thesis: verum
end;
end;
theorem Th63: :: TOPGEN_4:63
for T being non empty TopSpace
for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
proof
let T be non empty TopSpace; ::_thesis: for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
let X be Subset-Family of T; ::_thesis: ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
set V = { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
set Y = meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
A1: now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
X_c=_Z
let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies X c= Z )
assume Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: X c= Z
then ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
hence X c= Z ; ::_thesis: verum
end;
A2: bool the carrier of T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }
proof
set X1 = TotFam T;
TotFam T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
hence bool the carrier of T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: verum
end;
A3: for E being Subset of T st E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }
proof
let E be Subset of T; ::_thesis: ( E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } )
assume A4: E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
E_`_in_Z
let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies E ` in Z )
assume Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: E ` in Z
then ( E in Z & ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ) by A4, SETFAM_1:def_1;
hence E ` in Z by PROB_1:def_1; ::_thesis: verum
end;
hence E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A2, SETFAM_1:def_1; ::_thesis: verum
end;
A5: for BSeq being SetSequence of the carrier of T st rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }
proof
let BSeq be SetSequence of the carrier of T; ::_thesis: ( rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } )
assume A6: rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
Intersection_BSeq_in_Z
let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies Intersection BSeq in Z )
assume A7: Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: Intersection BSeq in Z
then consider S being Subset-Family of T such that
A8: Z = S and
X c= S and
A9: S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ;
now__::_thesis:_for_n_being_Nat_holds_BSeq_._n_in_Z
let n be Nat; ::_thesis: BSeq . n in Z
BSeq . n in rng BSeq by NAT_1:51;
hence BSeq . n in Z by A6, A7, SETFAM_1:def_1; ::_thesis: verum
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; ::_thesis: verum
end;
hence Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A2, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
{}_in_Z
let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies {} in Z )
assume Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: {} in Z
then ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing 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; ::_thesis: verum
end;
then {} in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A2, SETFAM_1:def_1;
then reconsider Y = meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } 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; ::_thesis: ( A is open implies A in Y )
assume A11: A is open ; ::_thesis: A in Y
for Y being set st Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
A in Y
proof
let Y be set ; ::_thesis: ( Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies A in Y )
assume Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; ::_thesis: A in Y
then ex S being Subset-Family of the carrier of T st
( Y = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
hence A in Y by A11, Def2; ::_thesis: verum
end;
hence A in Y by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider Y = Y as compl-closed all-open-containing closed_for_countable_unions Subset-Family of T by Def2;
take Y ; ::_thesis: ( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
for Z being set st X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
Y c= Z
proof
let Z be set ; ::_thesis: ( X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T implies Y c= Z )
assume that
A12: X c= Z and
A13: Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ; ::_thesis: Y c= Z
reconsider Z = Z as Subset-Family of T by A13;
Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A12, A13;
hence Y c= Z by SETFAM_1:3; ::_thesis: verum
end;
hence ( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
func BorelSets T -> compl-closed all-open-containing closed_for_countable_unions Subset-Family of T means :Def11: :: TOPGEN_4:def 11
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;
existence
ex b1 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G
proof
reconsider E = {} as Subset-Family of T by Th18;
consider Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T such that
E c= Y and
A1: for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st E c= Z holds
Y c= Z by Th63;
take Y ; ::_thesis: for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds Y c= G
let G be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; ::_thesis: Y c= G
thus Y c= G by A1, XBOOLE_1:2; ::_thesis: verum
end;
uniqueness
for b1, b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G ) holds
b1 = b2
proof
let R1, R2 be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; ::_thesis: ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) implies R1 = R2 )
assume ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) ) ; ::_thesis: R1 = R2
then ( R1 c= R2 & R2 c= R1 ) ;
hence R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines BorelSets TOPGEN_4:def_11_:_
for T being non empty TopSpace
for b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
( b2 = BorelSets T iff for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G );
theorem Th64: :: TOPGEN_4:64
for T being non empty TopSpace
for F being closed Subset-Family of T holds F c= BorelSets T
proof
let T be non empty TopSpace; ::_thesis: for F being closed Subset-Family of T holds F c= BorelSets T
let F be closed Subset-Family of T; ::_thesis: F c= BorelSets T
F c= BorelSets T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in BorelSets T )
assume A1: x in F ; ::_thesis: x in BorelSets T
then reconsider xx = x as Subset of T ;
xx is closed by A1, TOPS_2:def_2;
hence x in BorelSets T by Def3; ::_thesis: verum
end;
hence F c= BorelSets T ; ::_thesis: verum
end;
theorem Th65: :: TOPGEN_4:65
for T being non empty TopSpace
for F being open Subset-Family of T holds F c= BorelSets T
proof
let T be non empty TopSpace; ::_thesis: for F being open Subset-Family of T holds F c= BorelSets T
let F be open Subset-Family of T; ::_thesis: F c= BorelSets T
F c= BorelSets T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in BorelSets T )
assume A1: x in F ; ::_thesis: x in BorelSets T
then reconsider xx = x as Subset of T ;
xx is open by A1, TOPS_2:def_1;
hence x in BorelSets T by Def2; ::_thesis: verum
end;
hence F c= BorelSets T ; ::_thesis: verum
end;
theorem :: TOPGEN_4:66
for T being non empty TopSpace holds BorelSets T = sigma (Topology_of T)
proof
let T be non empty TopSpace; ::_thesis: BorelSets T = sigma (Topology_of T)
reconsider BT = BorelSets T as SigmaField of T by Th13;
set X = Topology_of T;
A1: for Z being set st Topology_of T c= Z & Z is SigmaField of T holds
BT c= Z
proof
let Z be set ; ::_thesis: ( Topology_of T c= Z & Z is SigmaField of T implies BT c= Z )
assume that
A2: Topology_of T c= Z and
A3: Z is SigmaField of T ; ::_thesis: BT c= Z
reconsider Z9 = Z as SigmaField of T by A3;
Z9 is all-open-containing by A2, Th59;
hence BT c= Z by Def11; ::_thesis: verum
end;
Topology_of T c= BT by Th65;
hence BorelSets T = sigma (Topology_of T) by A1, PROB_1:def_9; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
let A be Subset of T;
attrA is Borel means :Def12: :: TOPGEN_4:def 12
A in BorelSets T;
end;
:: deftheorem Def12 defines Borel TOPGEN_4:def_12_:_
for T being non empty TopSpace
for A being Subset of T holds
( A is Borel iff A in BorelSets T );
registration
let T be non empty TopSpace;
cluster F_sigma -> Borel for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is F_sigma holds
b1 is Borel
proof
let A be Subset of T; ::_thesis: ( A is F_sigma implies A is Borel )
assume A is F_sigma ; ::_thesis: A is Borel
then consider F being countable closed Subset-Family of T such that
A1: A = union F by Def6;
F c= BorelSets T by Th64;
then A in BorelSets T by A1, Def4;
hence A is Borel by Def12; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
cluster G_delta -> Borel for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is G_delta holds
b1 is Borel
proof
let A be Subset of T; ::_thesis: ( A is G_delta implies A is Borel )
assume A is G_delta ; ::_thesis: A is Borel
then consider F being countable open Subset-Family of T such that
A1: A = meet F by Def7;
F c= BorelSets T by Th65;
then A in BorelSets T by A1, Def5;
hence A is Borel by Def12; ::_thesis: verum
end;
end;