:: Basic Properties of Metrizable Topological Spaces
:: by Karol P\c{a}k
::
:: Received March 31, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, SUBSET_1, SETFAM_1, PCOMPS_1, CARD_1,
FINSET_1, T_0TOPSP, RELAT_1, XBOOLE_0, FUNCT_1, RCOMP_1, ORDINAL2,
TOPS_2, WAYBEL23, TARSKI, RLVECT_3, STRUCT_0, ZFMISC_1, XXREAL_0,
ARYTM_3, METRIC_1, CARD_5, NAGATA_1, TOPREAL7, CARD_2, MCART_1, ORDINAL1,
WEIERSTR, TOPMETR, ARYTM_1, COMPLEX1, XXREAL_1, TOPGEN_4, NAT_1, NEWTON,
CARD_3, NATTRA_1, TOPGEN_1, TOPS_1, REAL_1, FUNCOP_1, EUCLID, FINSEQ_2,
FINSEQ_1, CONNSP_1, METRIZTS;
notations BINOP_1, TOPMETR, CARD_1, CANTOR_1, COMPLEX1, FINSET_1, TARSKI,
XBOOLE_0, RELAT_1, SUBSET_1, ORDINAL1, NUMBERS, ZFMISC_1, XREAL_0,
REAL_1, DOMAIN_1, METRIC_1, PCOMPS_1, CARD_3, KURATO_0, WAYBEL23,
TOPGEN_1, FUNCOP_1, XCMPLX_0, TOPS_1, CARD_2, NEWTON, BORSUK_1, NAGATA_1,
TEX_2, TOPGEN_4, RCOMP_1, WEIERSTR, TOPREAL7, ORDERS_4, XXREAL_0,
FUNCT_1, RELSET_1, FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, SETFAM_1, STRUCT_0,
PRE_TOPC, CONNSP_1, TOPS_2, BORSUK_3, EUCLID, FINSEQ_2;
constructors REAL_1, CANTOR_1, TOPGEN_4, WAYBEL23, TOPGEN_1, TOPS_1, FUNCT_3,
TOPREAL9, CARD_2, NEWTON, CARD_5, NAGATA_1, TEX_2, CONNSP_1, RCOMP_1,
WEIERSTR, TOPREAL7, ORDERS_4, TOPS_2, BORSUK_3, FUNCSDOM, KURATO_0,
BINOP_2;
registrations TOPMETR, PRE_TOPC, PCOMPS_1, XREAL_0, SUBSET_1, STRUCT_0,
TOPS_1, METRIC_1, XXREAL_0, YELLOW13, CARD_1, XBOOLE_0, FINSET_1,
FUNCT_1, ORDINAL1, COMPTS_1, RELAT_1, XCMPLX_0, CARD_LAR, BORSUK_1,
TOPGEN_4, TOPREAL7, EUCLID, RELSET_1, VALUED_0, NEWTON, BINOP_2,
XTUPLE_0;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions PCOMPS_1, PRE_TOPC, TARSKI, TOPS_2, XBOOLE_0;
equalities BINOP_1, CARD_3, METRIC_1, PCOMPS_1, SUBSET_1, STRUCT_0, ORDINAL1;
expansions CARD_3, PRE_TOPC, TARSKI, TOPS_2, XBOOLE_0;
theorems ABSVALUE, BORSUK_1, BORSUK_5, CARD_1, CARD_2, CARD_3, CARD_4,
COMPL_SP, CONNSP_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_3, HAUSDORF,
JGRAPH_2, JORDAN1K, METRIC_1, NAGATA_1, NAGATA_2, NEWTON, PARTIT1,
PCOMPS_1, PCOMPS_2, PREPOWER, PRE_TOPC, PROB_1, SETFAM_1, SUBSET_1,
TARSKI, TEX_2, TMAP_1, TOPGEN_1, TOPGEN_2, TOPGEN_4, TOPMETR, TOPREAL7,
TOPS_1, TOPS_2, TSEP_1, TSP_1, WAYBEL23, WAYBEL29, XBOOLE_0, XBOOLE_1,
XREAL_1, XXREAL_0, XXREAL_1, YELLOW12, YELLOW_9, ZFMISC_1, T_0TOPSP,
TOPGRP_1, RELAT_1, ORDERS_4, NUMBERS, TOPREAL6, TOPREALA, EUCLID,
ORDINAL1, FINSEQ_2, YELLOW14, TOPS_3;
schemes BORSUK_2, CLASSES1, FRAENKEL, FUNCT_2, LMOD_7, NAT_1;
begin :: Preliminaries
reserve T, T1, T2 for TopSpace,
A, B for Subset of T,
F, G for Subset-Family of T,
A1 for Subset of T1,
A2 for Subset of T2,
TM, TM1, TM2 for metrizable TopSpace,
Am, Bm for Subset of TM,
Fm, Gm for Subset-Family of TM,
C for Cardinal,
iC for infinite Cardinal;
definition
let T1,T2,A1,A2;
pred A1,A2 are_homeomorphic means
T1|A1,T2|A2 are_homeomorphic;
end;
Lm1: for T1,T2 be empty TopSpace holds T1,T2 are_homeomorphic
proof
let T1,T2 be empty TopSpace;
reconsider E={} as Function of T1,T2 by FUNCT_2:1,RELAT_1:38;
A1: E" is continuous;
E is continuous;
then E is being_homeomorphism by A1;
hence thesis by T_0TOPSP:def 1;
end;
theorem
T1,T2 are_homeomorphic iff [#]T1,[#]T2 are_homeomorphic
proof
A1: T1|([#]T1)=the TopStruct of T1 & T2|([#]T2)=the TopStruct of T2 by
TSEP_1:93;
per cases;
suppose
A2: T2 is non empty;
thus T1,T2 are_homeomorphic implies [#]T1,[#]T2 are_homeomorphic
by A1,A2,TOPREALA:15;
assume [#]T1,[#]T2 are_homeomorphic;
then the TopStruct of T1,the TopStruct of T2 are_homeomorphic by A1;
hence thesis by A2,TOPREALA:15;
end;
suppose
A3: T2 is empty;
hereby
assume T1,T2 are_homeomorphic;
then T1 is empty iff T2 is empty by YELLOW14:18;
then T1|([#]T1),T2|([#]T2) are_homeomorphic by A3,Lm1;
hence [#]T1,[#]T2 are_homeomorphic;
end;
assume [#]T1,[#]T2 are_homeomorphic;
then T1|([#]T1),T2|([#]T2) are_homeomorphic;
then T1 is empty by A3,YELLOW14:18;
hence thesis by A3,Lm1;
end;
end;
theorem Th2:
for f be Function of T1,T2 st f is being_homeomorphism for g be
Function of T1|A1,T2|(f.:A1) st g = f|A1 holds g is being_homeomorphism
proof
let f be Function of T1,T2 such that
A1: f is being_homeomorphism;
A2: dom f=[#]T1 by A1;
T1,T2 are_homeomorphic by A1,T_0TOPSP:def 1;
then T1 is empty iff T2 is empty by YELLOW14:18;
then
A3: [#]T1={} iff [#]T2={};
A4: rng f=[#]T2 by A1;
set B= f.:A1;
let g be Function of T1|A1,T2|B such that
A5: g=f|A1;
A6: rng g=B by A5,RELAT_1:115;
A7: f is one-to-one by A1;
then
A8: g is one-to-one by A5,FUNCT_1:52;
A9: dom g = dom f/\A1 by A5,RELAT_1:61
.= A1 by A2,XBOOLE_1:28;
set TA=T1|A1,TB=T2|B;
A10: [#]TA=A1 by PRE_TOPC:def 5;
A11: [#]TA={} iff [#]TB={} by A9;
A12: [#]TB=B by PRE_TOPC:def 5;
A13: f is continuous by A1;
for P be Subset of TB st P is open holds g"P is open
proof
let P be Subset of TB;
assume P is open;
then consider P1 be Subset of T2 such that
A14: P1 is open and
A15: P=P1/\B by A12,TSP_1:def 1;
reconsider PA=f"P1/\A1 as Subset of TA by A10,XBOOLE_1:17;
A1=f"B by A2,A7,FUNCT_1:94;
then A1/\PA=PA & PA=f"P by A15,FUNCT_1:68,XBOOLE_1:17,28;
then
A16: g"P=PA by A5,FUNCT_1:70;
f"P1 is open by A3,A13,A14,TOPS_2:43;
hence thesis by A10,A16,TSP_1:def 1;
end;
then
A17: g is continuous by A11,TOPS_2:43;
A18: f" is continuous by A1;
for P be Subset of TA st P is open holds(g")"P is open
proof
let P be Subset of TA;
assume P is open;
then consider P1 be Subset of T1 such that
A19: P1 is open and
A20: P=P1/\A1 by A10,TSP_1:def 1;
reconsider PB=(f")"P1/\B as Subset of TB by A12,XBOOLE_1:17;
A21: (f")"P1 is open by A3,A18,A19,TOPS_2:43;
B = (f")"A1 by A4,A7,TOPS_2:54;
then PB = (f")"(P1/\A1) by FUNCT_1:68
.= f.:P by A4,A7,A20,TOPS_2:54
.= g.:P by A5,A10,RELAT_1:129
.= (g")"P by A6,A8,A12,TOPS_2:54;
hence thesis by A12,A21,TSP_1:def 1;
end;
then g" is continuous by A11,TOPS_2:43;
hence thesis by A6,A9,A10,A8,A12,A17;
end;
theorem
for f be Function of T1,T2 st f is being_homeomorphism holds A1,f.:A1
are_homeomorphic
proof
let f be Function of T1,T2 such that
A1: f is being_homeomorphism;
dom f=[#]T1 by A1;
then
A2: dom(f|A1) = [#]T1/\A1 by RELAT_1:61
.= A1 by XBOOLE_1:28
.= [#](T1|A1) by PRE_TOPC:def 5;
rng(f|A1) = f.:A1 by RELAT_1:115
.= [#](T2|(f.:A1)) by PRE_TOPC:def 5;
then reconsider g=f|A1 as Function of T1|A1,T2|(f.:A1) by A2,FUNCT_2:1;
g is being_homeomorphism by A1,Th2;
then T1|A1,T2|(f.:A1)are_homeomorphic by T_0TOPSP:def 1;
hence thesis;
end;
Lm2: for T1,T2 be non empty TopSpace st T1,T2 are_homeomorphic holds weight T2
c=weight T1
proof
let T1,T2 be non empty TopSpace;
defpred P[object] means not contradiction;
consider B1 be Basis of T1 such that
A1: card B1=weight T1 by WAYBEL23:74;
assume T1,T2 are_homeomorphic;
then consider f be Function of T1,T2 such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
deffunc F(Subset of T1)=f.:$1;
defpred PP[object] means $1 in B1 & P[$1];
A3: card{F(w) where w is Subset of T1:PP[w]}c=card B1 from BORSUK_2:sch 1;
consider B2 be Subset-Family of T2 such that
A4: B2={F(w) where w is Subset of T1:PP[w]} from LMOD_7:sch 5;
A5: for A be Subset of T2 st A is open for p be Point of T2 st p in A ex a
be Subset of T2 st a in B2 & p in a & a c=A
proof
let A be Subset of T2;
assume A is open;
then
A6: f"A is open by A2,TOPGRP_1:26;
let p be Point of T2 such that
A7: p in A;
A8: rng f=[#]T2 by A2;
then consider x be object such that
A9: x in dom f and
A10: f.x=p by FUNCT_1:def 3;
A11: x in f"A by A7,A9,A10,FUNCT_1:def 7;
reconsider x as Point of T1 by A9;
consider a1 be Subset of T1 such that
A12: a1 in B1 & x in a1 and
A13: a1 c=f"A by A6,A11,YELLOW_9:31;
take a=F(a1);
a c=f.:(f"A) by A13,RELAT_1:123;
hence thesis by A4,A8,A9,A10,A12,FUNCT_1:77,def 6;
end;
A14: B1 c=the topology of T1 by TOPS_2:64;
B2 c=the topology of T2
proof
let x be object;
assume x in B2;
then consider w be Subset of T1 such that
A15: x=F(w) and
A16: PP[w] by A4;
w is open by A14,A16;
then F(w) is open by A2,TOPGRP_1:25;
hence thesis by A15;
end;
then reconsider B2 as Basis of T2 by A5,YELLOW_9:32;
weight T2 c=card B2 by WAYBEL23:73;
hence thesis by A1,A4,A3;
end;
Lm3: for T be empty TopSpace holds weight T is empty
proof
let T be empty TopSpace;
reconsider B={} as empty Subset-Family of T by TOPGEN_4:18;
B c=the topology of T & for A be Subset of T st A is open for p be Point
of T st p in A ex a be Subset of T st a in B & p in a & a c=A;
then reconsider B as Basis of T by YELLOW_9:32;
weight T c=card B by WAYBEL23:73;
hence thesis;
end;
theorem Th4:
T1,T2 are_homeomorphic implies weight T1 = weight T2
proof
assume
A1: T1,T2 are_homeomorphic;
per cases;
suppose
A2: [#]T1={} or [#]T2={};
A3: T1 is empty iff T2 is empty by A1,YELLOW14:18;
then weight T1=0 by A2,Lm3;
hence thesis by A2,A3,Lm3;
end;
suppose
T1 is non empty & T2 is non empty;
then weight T2 c=weight T1 & weight T1 c=weight T2 by A1,Lm2;
hence thesis;
end;
end;
registration
cluster empty -> metrizable for TopSpace;
coherence
proof
let T be TopSpace;
set cT=the carrier of T;
A1: dom{}={} & rng{}c=REAL;
assume
A2: T is empty;
then
A3: bool cT={{}} by ZFMISC_1:1;
cT = {} by A2;
then [:cT,cT:]={} by ZFMISC_1:90;
then reconsider E={} as Function of[:cT,cT:],REAL by A1,FUNCT_2:2;
set M=SpaceMetr(cT,E);
take E;
thus E is_metric_of cT
proof let a,b,c be Element of cT;
A4: a=0 & b=0 by A2,SUBSET_1:def 1;
thus
E.(a,b)=0 iff a=b by A4;
thus E.(a,b)=E.(b,a) by A4;
E.(a,b) = 0;
hence E.(a,c)<=E.(a,b)+E.(b,c);
end;
then
A5: M=MetrStruct(# cT,E #) by PCOMPS_1:def 7;
then cT in Family_open_set(M) by PCOMPS_1:30;
then Family_open_set(M)={{}} by A3,A5,ZFMISC_1:33;
hence thesis by A3,ZFMISC_1:33;
end;
cluster metrizable -> T_4 for TopSpace;
coherence
proof
let T be TopSpace such that
A6: T is metrizable;
per cases;
suppose
A7: T is empty;
then for F1,F2 being Subset of T st F1 is closed & F2 is closed & F1
misses F2 ex G1,G2 be Subset of T st G1 is open & G2 is open & F1 c=G1 & F2 c=
G2 & G1 misses G2;
then T is normal;
hence thesis by A7;
end;
suppose
T is non empty;
then reconsider t=T as metrizable non empty TopSpace by A6;
t is regular & ex Bn being FamilySequence of t st Bn is
Basis_sigma_locally_finite by NAGATA_2:19;
then t is T_1 & T is normal by NAGATA_1:20,NAGATA_2:19;
hence thesis;
end;
end;
let M be MetrSpace;
cluster TopSpaceMetr M -> metrizable;
coherence
proof
per cases;
suppose
M is empty;
then TopSpaceMetr(M) is empty;
hence thesis;
end;
suppose
M is non empty;
then reconsider m=M as non empty MetrSpace;
set TM=TopSpaceMetr(M);
reconsider CM=[#]M as non empty Subset of m;
reconsider CTM=[#]TM as Subset of TM;
set TMM=TopSpaceMetr(m|CM);
A8: [#](m|CM)=CM by TOPMETR:def 2;
then reconsider
D=the distance of m|CM as Function of [:the carrier of TM,the
carrier of TM:],REAL;
take D;
A9: D is_metric_of the carrier of TM by A8,PCOMPS_1:35;
TM|CTM=TMM & TM is SubSpace of TM by HAUSDORF:16,TSEP_1:2;
then
the topology of TopSpaceMetr M = the topology of TopSpaceMetr(m|CM)
by A8,TSEP_1:5
.= Family_open_set(SpaceMetr(the carrier of TM,D)) by A8,A9,
PCOMPS_1:def 7;
hence thesis by A8,PCOMPS_1:35;
end;
end;
end;
registration
let TM,Am;
cluster TM|Am -> metrizable;
coherence
proof
per cases;
suppose
Am is empty;
hence thesis;
end;
suppose
A1: Am is non empty;
consider metr be Function of[:the carrier of TM,the carrier of TM:],
REAL such that
A2: metr is_metric_of the carrier of TM and
A3: Family_open_set(SpaceMetr(the carrier of TM,metr)) = the
topology of TM by PCOMPS_1:def 8;
A4: TM is non empty by A1;
then reconsider
TMM=SpaceMetr(the carrier of TM,metr) as non empty MetrSpace
by A2,PCOMPS_1:36;
reconsider Atm=Am as non empty Subset of TMM by A1,A2,A4,PCOMPS_2:4;
reconsider ATM=Atm as non empty Subset of TopSpaceMetr TMM;
TM is SubSpace of TM & the carrier of TopSpaceMetr TMM = the carrier
of TM by A2,A4,PCOMPS_2:4,TSEP_1:2;
then TopSpaceMetr TMM is SubSpace of TM by A3,TMAP_1:6;
then
A5: (TopSpaceMetr TMM)|ATM is SubSpace of TM by TSEP_1:7;
(TopSpaceMetr TMM)|ATM = TopSpaceMetr(TMM|Atm) & [#]((TopSpaceMetr
TMM)|ATM) = ATM by HAUSDORF:16,PRE_TOPC:def 5;
hence thesis by A5,PRE_TOPC:def 5;
end;
end;
end;
registration
let TM1,TM2;
cluster [:TM1,TM2:] -> metrizable;
coherence
proof
per cases;
suppose
[:TM1,TM2:] is empty;
hence thesis;
end;
suppose
A1: [:TM1,TM2:] is non empty;
then
A2: TM2 is non empty;
consider metr2 be Function of[:the carrier of TM2, the carrier of TM2:],
REAL such that
A3: metr2 is_metric_of the carrier of TM2 and
A4: Family_open_set(SpaceMetr(the carrier of TM2,metr2)) = the
topology of TM2 by PCOMPS_1:def 8;
set tm2=SpaceMetr(the carrier of TM2,metr2);
consider metr1 be Function of [:the carrier of TM1, the carrier of TM1:]
,REAL such that
A5: metr1 is_metric_of the carrier of TM1 and
A6: Family_open_set(SpaceMetr(the carrier of TM1,metr1)) = the
topology of TM1 by PCOMPS_1:def 8;
set tm1=SpaceMetr(the carrier of TM1,metr1);
A7: TM1 is non empty by A1;
then reconsider tm1,tm2 as non empty MetrStruct by A5,A3,A2,PCOMPS_1:36;
A8: the TopStruct of TM2=the TopStruct of TopSpaceMetr(tm2) by A3,A4,A2,
PCOMPS_2:4;
the TopStruct of TM1=the TopStruct of TopSpaceMetr(tm1) by A7,A5,A6,
PCOMPS_2:4;
then [:TM1,TM2:] = [:TopSpaceMetr(tm1),TopSpaceMetr(tm2):] by A8,
WAYBEL29:7
.= TopSpaceMetr max-Prod2(tm1,tm2) by TOPREAL7:23;
hence thesis;
end;
end;
end;
registration
let T be empty TopSpace;
cluster weight T -> empty;
coherence by Lm3;
end;
theorem Th5:
weight [:T1,T2:] c= weight T1 *` weight T2
proof
per cases;
suppose
T1 is empty or T2 is empty;
hence thesis;
end;
suppose
A1: T1 is non empty & T2 is non empty;
consider B2 be Basis of T2 such that
A2: card B2=weight T2 by WAYBEL23:74;
consider B1 be Basis of T1 such that
A3: card B1=weight T1 by WAYBEL23:74;
reconsider B12={[:a,b:] where a is Subset of T1,b is Subset of T2: a in B1
& b in B2} as Basis of[:T1,T2:] by A1,YELLOW_9:40;
reconsider B1,B2,B12 as non empty set by A1,YELLOW12:34;
deffunc F(Element of[:B1,B2:])=[:$1`1,$1`2:];
A4: for x be Element of[:B1,B2:] holds F(x) is Element of B12
proof
let x be Element of[:B1,B2:];
x`1 in B1 & x`2 in B2;
then F(x) in B12;
hence thesis;
end;
consider f be Function of[:B1,B2:],B12 such that
A5: for x be Element of[:B1,B2:] holds f.x=F(x) from FUNCT_2:sch 9(A4);
A6: dom f=[:B1,B2:] by FUNCT_2:def 1;
B12 c=rng f
proof
let x be object;
assume x in B12;
then consider a be Subset of T1,b be Subset of T2 such that
A7: x=[:a,b:] and
A8: a in B1 & b in B2;
reconsider ab=[a,b] as Element of[:B1,B2:] by A8,ZFMISC_1:87;
[a,b]`1=a & [a,b]`2=b;
then x=f.ab by A5,A7;
hence thesis by A6,FUNCT_1:def 3;
end;
then
A9: weight[:T1,T2:]c=card B12 & card B12 c=card[:B1,B2:] by A6,CARD_1:12
,WAYBEL23:73;
card[:B1,B2:]=card[:card B1,card B2:] by CARD_2:7
.=(card B1)*`card B2 by CARD_2:def 2;
hence thesis by A3,A2,A9;
end;
end;
theorem Th6:
T1 is non empty & T2 is non empty implies weight T1 c= weight [:
T1,T2:] & weight T2 c= weight[:T1,T2:]
proof
defpred P[object] means not contradiction;
set PR2=pr2(the carrier of T1,the carrier of T2);
set PR1=pr1(the carrier of T1,the carrier of T2);
assume T1 is non empty & T2 is non empty;
then reconsider t1=T1,t2=T2 as non empty TopSpace;
reconsider T12=[:t1,t2:] as non empty TopSpace;
consider B12 be Basis of T12 such that
A1: card B12=weight T12 by WAYBEL23:74;
deffunc F1(Subset of T12)=PR1.:$1;
defpred PP[object] means $1 in B12 & P[$1];
consider B1 be Subset-Family of T1 such that
A2: B1={F1(w) where w is Subset of T12:PP[w]} from LMOD_7:sch 5;
A3: B12 c=the topology of T12 by TOPS_2:64;
A4: B1 c=the topology of T1
proof
let x be object;
assume x in B1;
then consider w be Subset of T12 such that
A5: x=F1(w) and
A6: PP[w] by A2;
w is open by A3,A6;
then F1(w) is open by BORSUK_1:18;
hence thesis by A5;
end;
for A be Subset of T1 st A is open for p be Point of T1 st p in A ex a
be Subset of T1 st a in B1 & p in a & a c=A
proof
let A be Subset of T1;
assume A is open;
then
A7: [:A,[#]T2:] is open by BORSUK_1:6;
set p2=the Point of T2;
A8: p2 in [#]t2;
let p1 be Point of T1;
assume p1 in A;
then
A9: [p1,p2] in [:A,[#]T2:] by A8,ZFMISC_1:87;
then reconsider p=[p1,p2] as Point of T12;
consider a12 be Subset of T12 such that
A10: a12 in B12 and
A11: p in a12 and
A12: a12 c=[:A,[#]T2:] by A7,A9,YELLOW_9:31;
p1 in [#]t1 & p2 in [#]t2;
then
A13: PR1.(p1,p2)=p1 by FUNCT_3:def 4;
a12 is open by A3,A10;
then reconsider a=F1(a12) as open Subset of T1 by BORSUK_1:18;
take a;
dom PR1 = [:[#]T1,[#]T2:] by FUNCT_3:def 4
.= [#]T12 by BORSUK_1:def 2;
hence a in B1 & p1 in a by A2,A10,A11,A13,FUNCT_1:def 6;
let y be object;
assume y in a;
then consider x be object such that
A14: x in dom PR1 and
A15: x in a12 & y=PR1.x by FUNCT_1:def 6;
consider x1,x2 be object such that
A16: x1 in [#]T1 & x2 in [#]T2 and
A17: x=[x1,x2] by A14,ZFMISC_1:def 2;
PR1.(x1,x2)=x1 by A16,FUNCT_3:def 4;
hence thesis by A12,A15,A17,ZFMISC_1:87;
end;
then reconsider B1 as Basis of T1 by A4,YELLOW_9:32;
A18: card{F1(w) where w is Subset of T12:PP[w]} c= card B12 from BORSUK_2:
sch 1;
weight t1 c=card B1 by WAYBEL23:73;
hence weight T1 c=weight[:T1,T2:] by A1,A2,A18;
deffunc F2(Subset of T12)=PR2.:$1;
consider B2 be Subset-Family of T2 such that
A19: B2={F2(w) where w is Subset of T12:PP[w]} from LMOD_7:sch 5;
A20: for A be Subset of T2 st A is open for p be Point of T2 st p in A ex a
be Subset of T2 st a in B2 & p in a & a c=A
proof
let A be Subset of T2;
assume A is open;
then
A21: [:[#]T1,A:] is open by BORSUK_1:6;
set p1=the Point of T1;
A22: p1 in [#]t1;
let p2 be Point of T2;
assume p2 in A;
then
A23: [p1,p2] in [:[#]T1,A:] by A22,ZFMISC_1:87;
then reconsider p=[p1,p2] as Point of T12;
consider a12 be Subset of T12 such that
A24: a12 in B12 and
A25: p in a12 and
A26: a12 c=[:[#]T1,A:] by A21,A23,YELLOW_9:31;
p1 in [#]t1 & p2 in [#]t2;
then
A27: PR2.(p1,p2)=p2 by FUNCT_3:def 5;
a12 is open by A3,A24;
then reconsider a=F2(a12) as open Subset of T2 by BORSUK_1:18;
take a;
dom PR2 = [:[#]T1,[#]T2:] by FUNCT_3:def 5
.= [#]T12 by BORSUK_1:def 2;
hence a in B2 & p2 in a by A19,A24,A25,A27,FUNCT_1:def 6;
let y be object;
assume y in a;
then consider x be object such that
A28: x in dom PR2 and
A29: x in a12 & y=PR2.x by FUNCT_1:def 6;
consider x1,x2 be object such that
A30: x1 in [#]T1 & x2 in [#]T2 and
A31: x=[x1,x2] by A28,ZFMISC_1:def 2;
PR2.(x1,x2)=x2 by A30,FUNCT_3:def 5;
hence thesis by A26,A29,A31,ZFMISC_1:87;
end;
B2 c=the topology of T2
proof
let x be object;
assume x in B2;
then consider w be Subset of T12 such that
A32: x=F2(w) and
A33: PP[w] by A19;
w is open by A3,A33;
then F2(w) is open by BORSUK_1:18;
hence thesis by A32;
end;
then reconsider B2 as Basis of T2 by A20,YELLOW_9:32;
A34: card{F2(w) where w is Subset of T12:PP[w]}c=card B12 from BORSUK_2:sch
1;
weight T2 c=card B2 by WAYBEL23:73;
hence thesis by A1,A19,A34;
end;
registration
let T1,T2 be second-countable TopSpace;
cluster [:T1,T2:] -> second-countable;
coherence
proof
weight T1 c=omega & weight T2 c=omega by WAYBEL23:def 6;
then
A1: weight T1*`weight T2 c=omega by CARD_2:90,CARD_4:6;
weight[:T1,T2:]c=weight T1 *` weight T2 by Th5;
then weight[:T1,T2:]c=omega by A1;
hence thesis by WAYBEL23:def 6;
end;
end;
theorem Th7:
card (F|A) c= card F
proof
set FA=F|A;
per cases;
suppose
FA is empty;
hence thesis;
end;
suppose
A1: FA is non empty;
deffunc F(set) = $1/\A;
A2: A=[#](T|A) by PRE_TOPC:def 5;
A3: for x be set st x in F holds F(x) in FA
proof
let x be set;
A4: F(x)c=A by XBOOLE_1:17;
assume x in F;
hence thesis by A2,A4,TOPS_2:def 3;
end;
consider g be Function of F,FA such that
A5: for x be set st x in F holds g.x=F(x) from FUNCT_2:sch 11(A3);
A6: dom g=F by A1,FUNCT_2:def 1;
FA c=rng g
proof
let x be object;
assume x in FA;
then consider B such that
A7: B in F and
A8: F(B)=x by TOPS_2:def 3;
x=g.B by A5,A7,A8;
hence thesis by A6,A7,FUNCT_1:def 3;
end;
hence thesis by A6,CARD_1:12;
end;
end;
theorem Th8:
for Bas be Basis of T holds Bas|A is Basis of T|A
proof
let Bas be Basis of T;
set BasA=Bas|A;
set TA=T|A;
A1: for U be Subset of TA st U is open for p be Point of TA st p in U ex a
be Subset of TA st a in BasA & p in a & a c=U
proof
let U be Subset of TA;
assume U is open;
then consider W be Subset of T such that
A2: W is open and
A3: U=W/\the carrier of TA by TSP_1:def 1;
let p be Point of TA such that
A4: p in U;
p in W by A3,A4,XBOOLE_0:def 4;
then consider Wb be Subset of T such that
A5: Wb in Bas and
A6: p in Wb and
A7: Wb c=W by A2,YELLOW_9:31;
A8: Wb/\A in BasA by A5,TOPS_2:31;
then reconsider WbA=Wb/\A as Subset of TA;
A9: [#]TA=A by PRE_TOPC:def 5;
then p in WbA by A4,A6,XBOOLE_0:def 4;
hence thesis by A3,A7,A8,A9,XBOOLE_1:26;
end;
BasA c=the topology of TA
proof
let x be object such that
A10: x in BasA;
reconsider U=x as Subset of TA by A10;
BasA is open by TOPS_2:37;
then U is open by A10;
hence thesis;
end;
hence thesis by A1,YELLOW_9:32;
end;
registration
let T be second-countable TopSpace;
let A be Subset of T;
cluster T|A -> second-countable;
coherence
proof
consider B be Basis of T such that
A1: card B=weight T by WAYBEL23:74;
B|A is Basis of T|A by Th8;
then
A2: weight(T|A)c=card(B|A) by WAYBEL23:73;
card(B|A)c=card B by Th7;
then weight T c=omega & weight(T|A)c=weight T by A1,A2,WAYBEL23:def 6;
then weight(T|A)c=omega;
hence thesis by WAYBEL23:def 6;
end;
end;
registration
let M be non empty MetrSpace;
let A be non empty Subset of TopSpaceMetr M;
cluster dist_min A -> continuous;
coherence
proof
set d=dist_min A;
set TM=TopSpaceMetr M;
A1: for P being Subset of R^1 st P is open holds d"P is open
proof
let P be Subset of R^1;
assume
A2: P is open;
for p be Point of M st p in d"P ex r be Real st r>0 & Ball(p,
r)c=d"P
proof
reconsider P9=P as open Subset of TopSpaceMetr(RealSpace) by A2,
TOPMETR:def 6;
let p be Point of M;
assume p in d"P;
then
A3: d.p in P by FUNCT_1:def 7;
then reconsider dp=d.p as Point of RealSpace by TOPMETR:def 6;
consider r be Real such that
A4: r>0 and
A5: Ball(dp,r)c=P9 by A3,TOPMETR:15;
take r;
thus r>0 by A4;
thus Ball(p,r)c=d"P
proof
let x be object;
assume
A6: x in Ball(p,r);
then reconsider q=x as Point of M;
A7: dist(p,q)<r by A6,METRIC_1:11;
A8: dom d=[#]M by FUNCT_2:def 1;
then d.q in rng d by FUNCT_1:def 3;
then reconsider dq=d.q as Point of RealSpace by TOPMETR:def 6;
d.q<=dist(q,p)+d.p by HAUSDORF:15;
then d.q-d.p<=dist(p,q) by XREAL_1:20;
then
A9: -dist(p,q)<=-(d.q-d.p) by XREAL_1:24;
d.p<=dist(p,q)+d.q by HAUSDORF:15;
then d.p-d.q<=dist(p,q) by XREAL_1:20;
then |.d.p-d.q.|<=dist(p,q) by A9,ABSVALUE:5;
then |.d.p-d.q.|<r by A7,XXREAL_0:2;
then dist(dp,dq)<r by METRIC_1:def 12;
then dq in Ball(dp,r) by METRIC_1:11;
hence thesis by A5,A8,FUNCT_1:def 7;
end;
end;
hence thesis by TOPMETR:15;
end;
[#]R^1={} implies [#]TM={};
hence thesis by A1,TOPS_2:43;
end;
end;
theorem :: General Topology Th 4.1.10
for B be Subset of T,F be Subset of T|A st F = B holds T|A|F = T|B
proof
let B be Subset of T,F be Subset of T|A such that
A1: F = B;
(T|A|F) is SubSpace of T & [#](T|A|F)=F by PRE_TOPC:def 5,TSEP_1:7;
hence thesis by A1,PRE_TOPC:def 5;
end;
Lm4: for M be non empty MetrSpace for A be non empty Subset of TopSpaceMetr M,
r be Real holds {p where p is Point of TopSpaceMetr M:(dist_min A).p<r}
is open Subset of TopSpaceMetr M
proof
let M be non empty MetrSpace;
set TM=TopSpaceMetr M;
let A be non empty Subset of TM,r be Real;
set d=dist_min A;
reconsider A=].-infty,r.[ as Subset of R^1 by TOPMETR:17;
set dA={p where p is Point of TM:d.p<r};
A1: dA c=d"A
proof
let x be object;
assume x in dA;
then consider p be Point of TM such that
A2: p=x and
A3: d.p<r;
dom d=[#]TM & d.p in A by A3,FUNCT_2:def 1,XXREAL_1:233;
hence thesis by A2,FUNCT_1:def 7;
end;
A4: d"A c=dA
proof
let x be object;
assume
A5: x in d"A;
then reconsider p=x as Point of TM;
d.p in A by A5,FUNCT_1:def 7;
then d.p<r by XXREAL_1:233;
hence thesis;
end;
A6: A is open by BORSUK_5:40;
[#]R^1={} implies [#]TM={};
then d"A is open by A6,TOPS_2:43;
hence thesis by A1,A4,XBOOLE_0:def 10;
end;
:: F_sigma and G_delta Types of Subsets
registration
let TM;
cluster open -> F_sigma for Subset of TM;
coherence
proof
set TOP=the topology of TM,cTM=the carrier of TM;
let Am;
assume
A1: Am is open;
per cases;
suppose
A2: TM is empty;
reconsider E={} as empty Subset-Family of TM by TOPGEN_4:18;
Am=union E by A2,ZFMISC_1:2;
hence thesis by TOPGEN_4:def 6;
end;
suppose
A3: TM is non empty;
per cases;
suppose
Am=[#]TM;
hence thesis by A3;
end;
suppose
A4: Am<>[#]TM;
consider metr be Function of[:cTM,cTM:],REAL such that
A5: metr is_metric_of cTM and
A6: Family_open_set(SpaceMetr(cTM,metr))=TOP by PCOMPS_1:def 8;
reconsider Tm=SpaceMetr(cTM,metr) as non empty MetrSpace by A3,A5,
PCOMPS_1:36;
set TTm=TopSpaceMetr Tm;
Am in the topology of TTm by A1,A6;
then reconsider a=Am as open Subset of TTm by PRE_TOPC:def 2;
({}TTm)`=[#]TTm;
then reconsider A9=a` as closed non empty Subset of TTm by A3,A4,A5,
PCOMPS_2:4;
defpred P[object,object] means
for n be Nat st n=$1 holds$2={p where p is
Point of TTm: (dist_min A9).p<1/(2|^n)};
A7: for x be object st x in NAT ex y be object st y in TOP & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
reconsider BallA={p where p is Point of TTm: (dist_min A9).p<1/(2|^n
)} as open Subset of TTm by Lm4;
take BallA;
thus thesis by A6,PRE_TOPC:def 2;
end;
consider p be sequence of TOP such that
A8: for x be object st x in NAT holds P[x,p.x] from FUNCT_2:sch 1(
A7);
reconsider RNG=rng p as open Subset-Family of TM by TOPS_2:11
,XBOOLE_1:1;
set Crng=COMPLEMENT(RNG);
A9: dom p=NAT by FUNCT_2:def 1;
A10: [#]TM=[#]TTm by A3,A5,PCOMPS_2:4;
A11: union Crng = Am
proof
hereby
let x be object;
assume
A12: x in union Crng;
then consider y be set such that
A13: x in y and
A14: y in COMPLEMENT(RNG) by TARSKI:def 4;
reconsider Y=y as Subset of TM by A14;
Y` in RNG by A14,SETFAM_1:def 7;
then consider n be object such that
A15: n in dom p and
A16: p.n=Y` by FUNCT_1:def 3;
reconsider n as Element of NAT by A15;
assume not x in Am;
then x in A9 by A10,A12,XBOOLE_0:def 5;
then
A17: 2|^n>0 & (dist_min A9).x=0 by HAUSDORF:5,PREPOWER:6;
Y`={q where q is Point of TTm:(dist_min A9).q<1/(2|^n)} by A8,A16;
then x in Y` by A10,A12,A17;
hence contradiction by A13,XBOOLE_0:def 5;
end;
let x be object;
assume
A18: x in Am;
then reconsider q=x as Point of TTm by A3,A5,PCOMPS_2:4;
Cl A9=A9 & not q in A9 by A18,PRE_TOPC:22,XBOOLE_0:def 5;
then
A19: (dist_min A9).q<>0 by HAUSDORF:8;
(dist_min A9).q>=0 by JORDAN1K:9;
then consider n be Nat such that
A20: 1/(2|^n)<=(dist_min A9).q by A19,PREPOWER:92;
A21: n in NAT by ORDINAL1:def 12;
p.n in RNG by A9,FUNCT_1:def 3,A21;
then reconsider pn=p.n as Subset of TM;
A22: pn={s where s is Point of TTm:(dist_min A9).s<1/(2|^n)} by A8,A21;
for s be Point of TTm st s=q holds not 1/(2|^n)>(dist_min A9).s
by A20;
then not q in pn by A22;
then
A23: q in pn` by A18,XBOOLE_0:def 5;
pn`` in RNG by A9,FUNCT_1:def 3,A21;
then pn` in Crng by SETFAM_1:def 7;
hence thesis by A23,TARSKI:def 4;
end;
Crng is closed & RNG is countable by A9,CARD_3:93,TOPS_2:10;
hence thesis by A11,TOPGEN_4:def 6;
end;
end;
end;
cluster closed -> G_delta for Subset of TM;
coherence
proof
let Am;
assume
A24: Am is closed;
per cases;
suppose
A25: TM is empty;
reconsider E={} as empty Subset-Family of TM by TOPGEN_4:18;
Am=meet E by A25,SETFAM_1:1;
hence thesis by TOPGEN_4:def 7;
end;
suppose
TM is non empty;
then Am`` is G_delta by A24,TOPGEN_4:37;
hence thesis;
end;
end;
end;
theorem
for F be Subset of T|B st A is F_sigma & F = A/\B holds F is F_sigma
proof
let F be Subset of T|B;
assume that
A1: A is F_sigma and
A2: F=A/\B;
consider G be closed countable Subset-Family of T such that
A3: A=union G by A1,TOPGEN_4:def 6;
A4: union(G|B)c=F
proof
let x be object;
assume x in union(G|B);
then consider g be set such that
A5: x in g and
A6: g in G|B by TARSKI:def 4;
consider h be Subset of T such that
A7: h in G and
A8: h/\B=g by A6,TOPS_2:def 3;
x in h by A5,A8,XBOOLE_0:def 4;
then
A9: x in A by A3,A7,TARSKI:def 4;
x in B by A5,A8,XBOOLE_0:def 4;
hence thesis by A2,A9,XBOOLE_0:def 4;
end;
card(G|B)c=card G & card G c=omega by Th7,CARD_3:def 14;
then card(G|B)c=omega;
then
A10: G|B is closed & G|B is countable by TOPS_2:38;
A/\B/\B = A/\(B/\B) by XBOOLE_1:16
.= F by A2;
then F c=union(G|B) by A3,TOPS_2:32,XBOOLE_1:17;
then F=union(G|B) by A4;
hence thesis by A10,TOPGEN_4:def 6;
end;
theorem
for F be Subset of T|B st A is G_delta & F = A/\B holds F is G_delta
proof
let F be Subset of T|B;
assume that
A1: A is G_delta and
A2: F = A/\B;
consider G be open countable Subset-Family of T such that
A3: A = meet G by A1,TOPGEN_4:def 7;
A4: meet(G|B) c= F
proof
let x be object;
assume
A5: x in meet(G|B);
then consider g be object such that
A6: g in G|B by SETFAM_1:1,XBOOLE_0:def 1;
reconsider g as Subset of T|B by A6;
A7: ex h be Subset of T st h in G & h/\B=g by A6,TOPS_2:def 3;
x in g by A5,A6,SETFAM_1:def 1;
then
A8: x in B by A7,XBOOLE_0:def 4;
now
let Y be set;
assume Y in G;
then Y/\B in G|B by TOPS_2:31;
then x in Y/\B by A5,SETFAM_1:def 1;
hence x in Y by XBOOLE_0:def 4;
end;
then x in A by A3,A7,SETFAM_1:def 1;
hence thesis by A2,A8,XBOOLE_0:def 4;
end;
card(G|B)c=card G & card G c=omega by Th7,CARD_3:def 14;
then card(G|B)c=omega;
then
A9: G|B is open & G|B is countable by TOPS_2:37;
F c=meet(G|B)
proof
let x be object;
assume
A10: x in F;
then
A11: x in A by A2,XBOOLE_0:def 4;
A12: x in B by A2,A10,XBOOLE_0:def 4;
A13: now
let f be set;
assume f in G|B;
then consider h be Subset of T such that
A14: h in G and
A15: h/\B=f by TOPS_2:def 3;
x in h by A3,A11,A14,SETFAM_1:def 1;
hence x in f by A12,A15,XBOOLE_0:def 4;
end;
ex y be object st y in G by A3,A11,SETFAM_1:1,XBOOLE_0:def 1;
then G|B is non empty by TOPS_2:31;
hence thesis by A13,SETFAM_1:def 1;
end;
then F=meet(G|B) by A4;
hence thesis by A9,TOPGEN_4:def 7;
end;
theorem Th12:
T is T_1 & A is discrete implies A is open Subset of T|(Cl A)
proof
assume that
A1: T is T_1 and
A2: A is discrete;
set TA=T|(Cl A);
A3: [#]TA=Cl A by PRE_TOPC:def 5;
A4: A c=Cl A by PRE_TOPC:18;
per cases;
suppose
TA is empty;
hence thesis by A3,PRE_TOPC:18;
end;
suppose
TA is non empty;
then reconsider TA as non empty TopSpace;
deffunc F(Element of TA)={$1};
defpred P[set] means $1 in A;
consider S be Subset-Family of TA such that
A5: S={F(x) where x is Element of TA:P[x]} from LMOD_7:sch 5;
A6: S is open
proof
let B be Subset of TA;
assume B in S;
then consider y be Element of TA such that
A7: B=F(y) and
A8: P[y] by A5;
reconsider x=y as Point of T by A8;
consider G be Subset of T such that
A9: G is open and
A10: A/\G={x} by A2,A8,TEX_2:26;
reconsider X={x} as Subset of T by A10;
T is non empty by A7;
then
A11: Cl X=X by A1,PRE_TOPC:22;
x in {x} by TARSKI:def 1;
then x in A & x in G by A10,XBOOLE_0:def 4;
then
A12: G/\Cl A<>{} by A4,XBOOLE_0:def 4;
G/\Cl A c=Cl X by A9,A10,TOPS_1:13;
then G/\Cl A=X by A11,A12,ZFMISC_1:33;
hence thesis by A3,A7,A9,TSP_1:def 1;
end;
union S=A
proof
hereby
let x be object;
assume x in union S;
then consider y be set such that
A13: x in y and
A14: y in S by TARSKI:def 4;
ex z be Element of TA st F(z)=y & P[z] by A5,A14;
hence x in A by A13,TARSKI:def 1;
end;
let x be object;
assume x in A;
then
A15: {x} in S by A3,A4,A5;
x in {x} by TARSKI:def 1;
hence thesis by A15,TARSKI:def 4;
end;
hence thesis by A6,TOPS_2:19;
end;
end;
Lm5: omega*`iC=iC
proof
omega c=iC by CARD_3:85;
then
A1: omega*`iC c=iC*`iC by CARD_2:90;
iC*`iC=iC & iC c=omega*`iC by CARD_2:95,CARD_4:15;
hence thesis by A1;
end;
theorem Th13:
for T st for F st F is open & F is Cover of T ex G st G c= F & G
is Cover of T & card G c= C holds for A st A is closed & A is discrete holds
card A c= C
proof
let T;
assume
A1: for F st F is open & F is Cover of T ex G st G c=F & G is Cover of T
& card G c=C;
set TOP=the topology of T;
let A such that
A2: A is closed and
A3: A is discrete;
A` in TOP by A2,PRE_TOPC:def 2;
then
A4: {A`}c=TOP by ZFMISC_1:31;
defpred Q[object,object] means ex D1 being set st D1 = $1 & {$2}=D1/\A;
defpred P[object,object] means ex D2 being set st D2 = $2 & A/\D2={$1};
A5: for x be object st x in A ex y be object st y in TOP & P[x,y]
proof
let x be object;
assume x in A;
then consider G be Subset of T such that
A6: G is open & A/\G={x} by A3,TEX_2:26;
take G;
thus thesis by A6;
end;
consider p be Function of A,TOP such that
A7: for x be object st x in A holds P[x,p.x] from FUNCT_2:sch 1(A5);
reconsider RNG=rng p,AA={A`} as open Subset-Family of T by A4,TOPS_2:11
,XBOOLE_1:1;
reconsider RngA=RNG\/AA as open Subset-Family of T by TOPS_2:13;
[#]T c=union RngA
proof
let x be object;
assume
A8: x in [#]T;
per cases;
suppose
A9: x in A;
dom p=A by FUNCT_2:def 1;
then p.x in rng p by A9,FUNCT_1:def 3;
then
A10: p.x in RngA by XBOOLE_0:def 3;
P[x,p.x] by A7,A9;
then x in {x} & A/\(p.x)={x} by TARSKI:def 1;
then x in p.x by XBOOLE_0:def 4;
hence thesis by A10,TARSKI:def 4;
end;
suppose
A11: not x in A;
A` in AA by TARSKI:def 1;
then
A12: A` in RngA by XBOOLE_0:def 3;
x in A` by A8,A11,XBOOLE_0:def 5;
hence thesis by A12,TARSKI:def 4;
end;
end;
then RngA is Cover of T by SETFAM_1:def 11;
then consider G be Subset-Family of T such that
A13: G c=RngA and
A14: G is Cover of T and
A15: card G c=C by A1;
A16: for x be object st x in G\AA ex y be object st y in A & Q[x,y]
proof
let x be object;
assume x in G\AA;
then x in G & not x in AA by XBOOLE_0:def 5;
then x in RNG by A13,XBOOLE_0:def 3;
then consider y be object such that
A17: y in dom p & p.y=x by FUNCT_1:def 3;
take y;
P[y,p.y] by A7,A17;
hence thesis by A17;
end;
consider q be Function of G\AA,A such that
A18: for x be object st x in G\AA holds Q[x,q.x] from FUNCT_2:sch 1(A16);
per cases;
suppose
A is empty;
hence thesis;
end;
suppose
A is non empty;
then
A19: dom q=G\AA by FUNCT_2:def 1;
A c=rng q
proof
let x be object such that
A20: x in A;
T is non empty by A20;
then consider U be Subset of T such that
A21: x in U and
A22: U in G by A14,A20,PCOMPS_1:3;
not x in A` by A20,XBOOLE_0:def 5;
then not U in AA by A21,TARSKI:def 1;
then
A23: U in G\AA by A22,XBOOLE_0:def 5;
then Q[U,q.U] by A18;
then
A24: q.U in rng q & {q.U}=U/\A by A19,FUNCT_1:def 3,A23;
x in A/\U by A20,A21,XBOOLE_0:def 4;
hence thesis by A24,TARSKI:def 1;
end;
then
A25: card A c=card(G\AA) by A19,CARD_1:12;
card(G\AA)c=card G by CARD_1:11,XBOOLE_1:36;
then card A c=card G by A25;
hence card A c=C by A15;
end;
end;
theorem Th14:
for TM st for Am st Am is closed & Am is discrete holds card Am
c= iC holds for Am st Am is discrete holds card Am c= iC
proof
let TM;
assume
A1: for Am st Am is closed & Am is discrete holds card Am c=iC;
let Am such that
A2: Am is discrete;
per cases;
suppose
Am is empty;
hence thesis;
end;
suppose
A3: Am is non empty;
then reconsider Tm=TM as metrizable non empty TopSpace;
Am c=Cl Am by PRE_TOPC:18;
then reconsider ClA=Cl Am as non empty closed Subset of Tm by A3;
set TA=Tm|ClA;
reconsider A9=Am as open Subset of TA by A2,Th12;
consider F be closed countable Subset-Family of TA such that
A4: A9=union F by TOPGEN_4:def 6;
consider f be sequence of F such that
A5: rng f=F by A3,A4,CARD_3:96,ZFMISC_1:2;
A6: for x be object st x in dom f holds card(f.x)c=iC
proof
let x be object;
assume x in dom f;
then
A7: f.x in rng f by FUNCT_1:def 3;
then reconsider fx=f.x as Subset of TA by A5;
A8: f.x c=Am by A4,A7,ZFMISC_1:74;
then reconsider Fx=f.x as Subset of TM by XBOOLE_1:1;
[#]TA=ClA & fx is closed by A7,PRE_TOPC:def 5,TOPS_2:def 2;
then Fx is closed by TSEP_1:8;
hence thesis by A1,A2,A8,TEX_2:22;
end;
card dom f=omega by A3,A4,CARD_1:47,FUNCT_2:def 1,ZFMISC_1:2;
then card Union f c=(omega)*`iC by A6,CARD_2:86;
hence thesis by A4,A5,Lm5;
end;
end;
theorem Th15:
for T st for A st A is discrete holds card A c= C
for F st F is open & not {} in F &
for A,B st A in F & B in F & A <> B holds A misses B holds card F c= C
proof
let T;
assume
A1: for A st A is discrete holds card A c=C;
let F such that
A2: F is open and
A3: not{} in F and
A4: for A,B st A in F & B in F & A<>B holds A misses B;
per cases;
suppose
F is empty;
hence thesis;
end;
suppose
A5: F is non empty;
deffunc P(set)=the Element of $1;
:: Choice !!! ???
A6: for x be set st x in F holds P(x) in [#]T
proof
let x be set;
assume
A7: x in F;
then x<>{} by A3;
then P(x) in x;
hence thesis by A7;
end;
consider p be Function of F,[#]T such that
A8: for x be set st x in F holds p.x=P(x) from FUNCT_2:sch 11(A6);
reconsider RNG=rng p as Subset of T;
ex xx be object st xx in F by A5;
then
A9: T is non empty by A3;
then
A10: dom p=F by FUNCT_2:def 1;
for x be Point of T st x in RNG ex G be Subset of T st G is open &
RNG/\G={x}
proof
let x be Point of T;
assume
A11: x in RNG;
then consider G be object such that
A12: G in F and
A13: p.G=x by A10,FUNCT_1:def 3;
reconsider G as Subset of T by A12;
A14: RNG/\G c={x}
proof
let y be object;
assume
A15: y in RNG/\G;
then
A16: y in G by XBOOLE_0:def 4;
y in RNG by A15,XBOOLE_0:def 4;
then consider z be object such that
A17: z in F and
A18: p.z=y by A10,FUNCT_1:def 3;
reconsider z as set by TARSKI:1;
y=P(z) by A8,A17,A18;
then z meets G by A3,A16,A17,XBOOLE_0:3;
then x=y by A4,A12,A13,A17,A18;
hence thesis by TARSKI:def 1;
end;
take G;
thus G is open by A2,A12;
x=P(G) by A8,A12,A13;
then x in RNG/\G by A3,A11,A12,XBOOLE_0:def 4;
hence thesis by A14,ZFMISC_1:33;
end;
then
A19: card RNG c=C by A1,A9,TEX_2:31;
for x1,x2 be object st x1 in dom p & x2 in dom p & p.x1=p.x2 holds x1=x2
proof
let x1,x2 be object such that
A20: x1 in dom p and
A21: x2 in dom p and
A22: p.x1=p.x2;
reconsider x1,x2 as set by TARSKI:1;
A23: p.x2=P(x2) & x2<>{} by A3,A8,A21;
p.x1=P(x1) & x1<>{} by A3,A8,A20;
then x1 meets x2 by A22,A23,XBOOLE_0:3;
hence thesis by A4,A10,A20,A21;
end;
then p is one-to-one by FUNCT_1:def 4;
then card F c=card RNG by A10,CARD_1:10;
hence thesis by A19;
end;
end;
theorem Th16:
for F st F is Cover of T ex G st G c= F & G is Cover of T & card
G c= card [#]T
proof
let F such that
A1: F is Cover of T;
per cases;
suppose
A2: F is empty;
take F;
thus thesis by A1,A2;
end;
suppose
A3: F is non empty;
defpred P[object,object] means ex D2 being set st D2 = $2 & $1 in D2;
A4: for x be object st x in [#]T ex y be object st y in F & P[x,y]
proof
let x be object;
assume x in [#]T;
then x in union F by A1,SETFAM_1:45;
then ex y be set st x in y & y in F by TARSKI:def 4;
hence thesis;
end;
consider g be Function of[#]T,F such that
A5: for x be object st x in [#]T holds P[x,g.x] from FUNCT_2:sch 1(A4);
reconsider R=rng g as Subset-Family of T by XBOOLE_1:1;
take R;
A6: dom g=[#]T by A3,FUNCT_2:def 1;
[#]T c=union R
proof
let x be object;
assume
A7: x in [#]T;
then P[x,g.x] by A5;
then x in g.x & g.x in R by A6,FUNCT_1:def 3,A7;
hence thesis by TARSKI:def 4;
end;
hence thesis by A6,CARD_1:12,SETFAM_1:def 11;
end;
end;
Lm6: (for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm &
Am<>Bm holds Am misses Bm holds card Fm c=iC) implies density TM c=iC
proof
assume
A1: for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in
Fm & Am<>Bm holds Am misses Bm holds card Fm c=iC;
per cases;
suppose
A2: TM is empty;
ex D be Subset of TM st D is dense & density TM=card D by TOPGEN_1:def 12;
hence thesis by A2;
end;
suppose
A3: TM is non empty;
consider metr be Function of[:the carrier of TM,the carrier of TM:],REAL
such that
A4: metr is_metric_of the carrier of TM and
A5: Family_open_set(SpaceMetr(the carrier of TM,metr))=the topology of
TM by PCOMPS_1:def 8;
reconsider M=SpaceMetr(the carrier of TM,metr) as non empty MetrSpace by A3
,A4,PCOMPS_1:36;
defpred P[object,object] means
for n be Nat st $1=n ex G be Subset of TM st G=$2
& card G c= iC & for p be Element of M ex q be Element of M st q in G & dist(p,
q)<1/(2|^n);
A6: the carrier of TM=the carrier of M by A3,A4,PCOMPS_2:4;
A7: for x be object st x in NAT
ex y be object st y in bool the carrier of TM & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
reconsider r=1/(2|^n) as Real;
A8: 2|^n>0 by PREPOWER:6;
then consider A be Subset of M such that
A9: for p,q be Point of M st p<>q & p in A & q in A holds dist(p,q) >=r and
A10: for p be Point of M ex q be Point of M st q in A & p in Ball(q,
r) by COMPL_SP:30;
set BALL={Ball(p,r/2) where p is Element of M:p in A};
A11: BALL c=the topology of TM
proof
let x be object;
assume x in BALL;
then ex p be Point of M st x=Ball(p,r/2) & p in A;
hence thesis by A5,PCOMPS_1:29;
end;
reconsider BALL as open Subset-Family of TM by A11,TOPS_2:11,XBOOLE_1:1;
defpred Q[object,object] means
for p be Point of M st Ball(p,r/2)=$1 & p in A
holds p=$2;
A12: for x be object st x in BALL ex y be object st y in A & Q[x,y]
proof
let x be object;
assume x in BALL;
then consider p be Point of M such that
A13: x=Ball(p,r/2) and
A14: p in A;
A15: r/2<r by A8,XREAL_1:216;
take p;
thus p in A by A14;
let q be Point of M such that
A16: Ball(q,r/2)=x and
A17: q in A;
dist(p,p)=0 by METRIC_1:1;
then p in Ball(p,r/2) by A8,METRIC_1:11;
then dist(q,p)<r/2 by A13,A16,METRIC_1:11;
then dist(q,p)<r by A15,XXREAL_0:2;
hence thesis by A9,A14,A17;
end;
consider f be Function of BALL,A such that
A18: for x be object st x in BALL holds Q[x,f.x] from FUNCT_2:sch 1(A12
);
reconsider RNG=rng f as Subset of TM by A6,XBOOLE_1:1;
ex q be Point of M st q in A & the Point of M in Ball(q,r) by A10;
then
A19: dom f=BALL by FUNCT_2:def 1;
then
A20: card RNG c=card BALL by CARD_1:12;
A21: for A9,B9 be Subset of TM st A9 in BALL & B9 in BALL & A9<>B9 holds
A9 misses B9
proof
let A9,B9 be Subset of TM such that
A22: A9 in BALL and
A23: B9 in BALL and
A24: A9<>B9;
consider b be Element of M such that
A25: Ball(b,r/2)=B9 and
A26: b in A by A23;
consider a be Element of M such that
A27: Ball(a,r/2)=A9 and
A28: a in A by A22;
assume A9 meets B9;
then consider x be object such that
A29: x in A9 and
A30: x in B9 by XBOOLE_0:3;
reconsider x as Element of M by A27,A29;
A31: dist(a,x)<r/2 by A27,A29,METRIC_1:11;
dist(b,x)<r/2 by A25,A30,METRIC_1:11;
then
A32: dist(a,b)<=dist(a,x)+dist(x,b) & dist(a,x)+dist(x,b)<r/2+r/2 by A31,
METRIC_1:4,XREAL_1:8;
dist(a,b)>=r by A9,A24,A25,A26,A27,A28;
hence thesis by A32,XXREAL_0:2;
end;
take RNG;
thus RNG in bool the carrier of TM;
let m be Nat such that
A33: x=m;
A34: now
let p be Element of M;
consider q be Point of M such that
A35: q in A and
A36: p in Ball(q,r) by A10;
take q;
A37: Ball(q,r/2) in BALL by A35;
then f.(Ball(q,r/2))=q by A18,A35;
hence q in RNG & dist(p,q)<1/(2|^m) by A19,A33,A36,A37,FUNCT_1:def 3
,METRIC_1:11;
end;
not {} in BALL
proof
assume {} in BALL;
then consider p be Element of M such that
A38: Ball(p,r/2)={} and
p in A;
dist(p,p)=0 by METRIC_1:1;
hence thesis by A8,A38,METRIC_1:11;
end;
then card BALL c=iC by A1,A21;
hence thesis by A20,A34,XBOOLE_1:1;
end;
consider p be sequence of bool the carrier of TM such that
A39: for x be object st x in NAT holds P[x,p.x] from FUNCT_2:sch 1(A7);
reconsider Up=Union p as Subset of TM;
for U be Subset of TM st U<>{} & U is open holds Up meets U
proof
let U be Subset of TM;
reconsider U9=U as Subset of M by A3,A4,PCOMPS_2:4;
assume that
A40: U<>{} and
A41: U is open;
consider q be object such that
A42: q in U by A40,XBOOLE_0:def 1;
reconsider q as Element of M by A3,A4,A42,PCOMPS_2:4;
U9 in Family_open_set(M) by A5,A41;
then consider r be Real such that
A43: r>0 and
A44: Ball(q,r)c=U9 by A42,PCOMPS_1:def 4;
consider n be Nat such that
A45: 1/(2|^n)<=r by A43,PREPOWER:92;
A46: n in NAT by ORDINAL1:def 12;
consider G be Subset of TM such that
A47: G=p.n and
card G c=iC and
A48: for p be Element of M ex q be Element of M st q in G & dist(p,q
)<1/(2|^n) by A39,A46;
consider qq be Element of M such that
A49: qq in G and
A50: dist(q,qq)<1/(2|^n) by A48;
dist(q,qq)<r by A45,A50,XXREAL_0:2;
then
A51: qq in Ball(q,r) by METRIC_1:11;
qq in Up by A47,A49,PROB_1:12;
hence thesis by A44,A51,XBOOLE_0:3;
end;
then Up is dense by TOPS_1:45;
then
A52: density TM c=card Up by TOPGEN_1:def 12;
A53: for x be object st x in dom p holds card(p.x)c=iC
proof
let x be object;
assume x in dom p;
then reconsider n=x as Element of NAT;
ex G be Subset of TM st G=p.n & card G c=iC & for p be Element of M
ex q be Element of M st q in G & dist(p,q)<1/(2|^n) by A39;
hence thesis;
end;
card dom p=omega by CARD_1:47,FUNCT_2:def 1;
then
A54: card Up c=omega*`iC by A53,CARD_2:86;
omega*`iC=iC by Lm5;
hence thesis by A52,A54;
end;
end;
theorem Th17:
Am is dense implies weight TM c= omega *` card Am
proof
assume
A1: Am is dense;
per cases;
suppose
TM is empty;
hence thesis;
end;
suppose
A2: TM is non empty;
set TOP=the topology of TM,cTM=the carrier of TM;
consider metr be Function of[:cTM,cTM:],REAL such that
A3: metr is_metric_of cTM and
A4: Family_open_set(SpaceMetr(cTM,metr))=TOP by PCOMPS_1:def 8;
reconsider Tm=SpaceMetr(cTM,metr) as non empty MetrSpace by A2,A3,
PCOMPS_1:36;
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for n be Nat st n = $1 holds $2={Ball(p,1/(2|^n))
where p is Point of Tm:p in Am} & card D2 c= card Am;
A5: for x be object st x in NAT ex y be object st y in bool TOP & P[x,y]
proof
defpred P[object] means not contradiction;
let x be object;
defpred P1[object] means $1 in Am;
defpred P2[object] means $1 in Am & P[$1];
assume x in NAT;
then reconsider n=x as Element of NAT;
deffunc F(Point of Tm)=Ball($1,1/(2|^n));
set BALL1={F(p) where p is Point of Tm:P1[p]};
set BALL2={F(p) where p is Point of Tm:P2[p]};
take BALL1;
A6: BALL1 c=TOP
proof
let y be object;
assume y in BALL1;
then ex p be Point of Tm st y=F(p) & P1[p];
hence thesis by A4,PCOMPS_1:29;
end;
A7: for p be Point of Tm holds P1[p] iff P2[p];
A8: BALL1=BALL2 from FRAENKEL:sch 3(A7);
thus BALL1 in bool TOP by A6;
take BALL1;
card BALL2 c=card Am from BORSUK_2:sch 1;
hence thesis by A8;
end;
consider P be sequence of bool TOP such that
A9: for x be object st x in NAT holds P[x,P.x] from FUNCT_2:sch 1(A5);
reconsider Up=Union P as Subset-Family of TM by XBOOLE_1:1;
A10: for B be Subset of TM st B is open for p be Point of TM st p in B ex
a be Subset of TM st a in Up & p in a & a c= B
proof
let B be Subset of TM;
assume B is open;
then
A11: B in TOP;
let p be Point of TM such that
A12: p in B;
reconsider p9=p as Point of Tm by A2,A3,PCOMPS_2:4;
consider r be Real such that
A13: r>0 and
A14: Ball(p9,r)c=B by A4,A11,A12,PCOMPS_1:def 4;
consider n be Nat such that
A15: 1/(2|^n)<=r/2 by A13,PREPOWER:92;
reconsider B2=Ball(p9,1/(2|^n)) as Subset of TM by A2,A3,PCOMPS_2:4;
2|^n>0 & dist(p9,p9)=0 by METRIC_1:1,PREPOWER:6;
then
A16: p9 in B2 by METRIC_1:11;
B2 in TOP by A4,PCOMPS_1:29;
then B2 is open;
then B2 meets Am by A1,A16,TOPS_1:45;
then consider q be object such that
A17: q in B2 and
A18: q in Am by XBOOLE_0:3;
A19: n in NAT by ORDINAL1:def 12;
reconsider q as Point of Tm by A17;
reconsider B3=Ball(q,1/(2|^n)) as Subset of TM by A2,A3,PCOMPS_2:4;
take B3;
P[n,P.n] by A9,A19;
then P.n={Ball(t,1/(2|^n)) where t is Point of Tm:t in Am};
then B3 in P.n by A18;
hence B3 in Up by PROB_1:12;
A20: dist(p9,q)<1/(2|^n) by A17,METRIC_1:11;
hence p in B3 by METRIC_1:11;
let y be object;
assume
A21: y in B3;
then reconsider t=y as Point of Tm;
dist(q,t)<1/(2|^n) by A21,METRIC_1:11;
then
A22: dist(q,t)<r/2 by A15,XXREAL_0:2;
dist(p9,q)<r/2 by A15,A20,XXREAL_0:2;
then dist(p9,t)<=dist(p9,q)+dist(q,t) & dist(p9,q)+dist(q,t)<r/2+r/2 by
A22,METRIC_1:4,XREAL_1:8;
then dist(p9,t)<r by XXREAL_0:2;
then t in Ball(p9,r) by METRIC_1:11;
hence thesis by A14;
end;
Up is Basis of TM by A10,YELLOW_9:32;
then
A23: weight TM c=card Up by WAYBEL23:73;
A24: card dom P=omega by CARD_1:47,FUNCT_2:def 1;
for x be object st x in dom P holds card(P.x)c=card Am
proof let x be object;
assume
A25: x in dom P;
then P[x,P.x] by A9;
hence thesis by A25;
end;
then card Union P c=(omega)*`card Am by A24,CARD_2:86;
hence thesis by A23;
end;
end;
Lm7: density TM c=iC implies weight TM c=iC
proof
consider A be Subset of TM such that
A1: A is dense and
A2: density TM=card A by TOPGEN_1:def 12;
A3: weight TM c=omega*`card A by A1,Th17;
assume density TM c=iC;
then omega*`card A c=omega*`iC by A2,CARD_2:90;
then weight TM c=omega*`iC by A3;
hence thesis by Lm5;
end;
begin :: Main Properties
:: General Topology Th 4.1.15 (a) <=> (c)
theorem Th18:
weight TM c= iC iff for Fm st Fm is open & Fm is Cover of TM ex
Gm st Gm c=Fm & Gm is Cover of TM & card Gm c= iC
proof
hereby
assume
A1: weight TM c=iC;
let F be Subset-Family of TM such that
A2: F is open and
A3: F is Cover of TM;
per cases;
suppose
A4: TM is empty;
reconsider G={} as Subset-Family of TM by TOPGEN_4:18;
take G;
the carrier of TM = {} by A4;
then [#]TM=union G;
hence G c=F & G is Cover of TM & card G c=iC by SETFAM_1:def 11;
end;
suppose
TM is non empty;
then consider G be open Subset-Family of TM such that
A5: G c=F & union G=union F & card G c=weight TM by A2,TOPGEN_2:11;
reconsider G as Subset-Family of TM;
take G;
union F=[#]TM by A3,SETFAM_1:45;
hence G c=F & G is Cover of TM & card G c=iC by A1,A5,SETFAM_1:def 11;
end;
end;
assume for F be Subset-Family of TM st F is open & F is Cover of TM ex G
be Subset-Family of TM st G c=F & G is Cover of TM & card G c=iC;
then for A be Subset of TM st A is closed & A is discrete holds card A c=iC
by Th13;
then for A be Subset of TM st A is discrete holds card A c=iC by Th14;
then for F be Subset-Family of TM st F is open & not{} in F & for A,B be
Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC by
Th15;
then density TM c=iC by Lm6;
hence thesis by Lm7;
end;
:: General Topology Th 4.1.15 (a) <=> (d)
theorem Th19:
weight TM c=iC iff for Am st Am is closed & Am is discrete holds
card Am c= iC
proof
hereby
assume weight TM c=iC;
then for Fm st Fm is open & Fm is Cover of TM ex Gm st Gm c=Fm & Gm is
Cover of TM & card Gm c=iC by Th18;
hence for Am st Am is closed & Am is discrete holds card Am c=iC by Th13;
end;
assume for Am st Am is closed & Am is discrete holds card Am c=iC;
then for Am st Am is discrete holds card Am c=iC by Th14;
then
for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm &
Am<>Bm holds Am misses Bm holds card Fm c=iC by Th15;
then density TM c=iC by Lm6;
hence thesis by Lm7;
end;
:: General Topology Th 4.1.15 (a) <=> (e)
theorem Th20:
weight TM c= iC iff for Am st Am is discrete holds card Am c= iC
proof
hereby
assume weight TM c=iC;
then
for A be Subset of TM st A is closed & A is discrete holds card A c=iC
by Th19;
hence for A be Subset of TM st A is discrete holds card A c=iC by Th14;
end;
assume for A be Subset of TM st A is discrete holds card A c=iC;
then for F be Subset-Family of TM st F is open & not{} in F & for A,B be
Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC by
Th15;
then density TM c=iC by Lm6;
hence thesis by Lm7;
end;
:: General Topology Th 4.1.15 (a) <=> (f)
theorem Th21:
weight TM c= iC iff for Fm st Fm is open & not{} in Fm & for Am,
Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds card Fm c= iC
proof
hereby
assume weight TM c=iC;
then for A be Subset of TM st A is discrete holds card A c=iC by Th20;
hence for F be Subset-Family of TM st F is open & not{} in F & for A,B be
Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c= iC by
Th15;
end;
assume for F be Subset-Family of TM st F is open & not{} in F & for A,B be
Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC;
then density TM c=iC by Lm6;
hence thesis by Lm7;
end;
:: General Topology Th 4.1.15 (a) <=> (g)
theorem Th22:
weight TM c= iC iff density TM c= iC
proof
consider A be Subset of TM such that
A1: A is dense and
A2: density TM=card A by TOPGEN_1:def 12;
hereby
assume weight TM c=iC;
then for F be Subset-Family of TM st F is open & not{} in F & for A,B be
Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC by
Th21;
hence density TM c=iC by Lm6;
end;
A3: weight TM c=omega*`card A by A1,Th17;
assume density TM c=iC;
then omega*`card A c=omega*`iC by A2,CARD_2:90;
then weight TM c=omega*`iC by A3;
hence thesis by Lm5;
end;
theorem Th23:
for B be Basis of TM st for Fm st Fm is open & Fm is Cover of TM
ex Gm st Gm c=Fm & Gm is Cover of TM & card Gm c= iC ex underB be Basis of TM
st underB c= B & card underB c= iC
proof
let B be Basis of TM such that
A1: for F being Subset-Family of TM st F is open & F is Cover of TM ex G
be Subset-Family of TM st G c=F & G is Cover of TM & card G c=iC;
per cases;
suppose
TM is empty;
then weight TM=0;
then consider underB be Basis of TM such that
A2: card underB=0 by WAYBEL23:74;
take underB;
underB={} by A2;
hence thesis;
end;
suppose
A3: TM is non empty;
set TOP=the topology of TM,cT=the carrier of TM;
consider metr be Function of[:cT,cT:],REAL such that
A4: metr is_metric_of cT and
A5: Family_open_set(SpaceMetr(cT,metr))=TOP by PCOMPS_1:def 8;
reconsider Tm=SpaceMetr(cT,metr) as non empty MetrSpace by A3,A4,
PCOMPS_1:36;
defpred P[object,object] means
for n be Nat st $1=n ex G be open Subset-Family
of TM st G c={U where U is Subset of TM: U in B & ex p be Point of Tm st U c=
Ball(p,1/(2|^n))} & G is Cover of TM & card G c= iC & $2 = G;
A6: B c= TOP by TOPS_2:64;
A7: for x be object st x in NAT ex y be object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Nat;
set F={U where U is Subset of TM:U in B & ex p be Element of Tm st U c=
Ball (p,1/(2|^n))};
A8: F c=TOP
proof
let f be object;
assume f in F;
then ex U be Subset of TM st f=U & U in B & ex p be Point of Tm st U
c= Ball(p,1/(2|^n));
hence thesis by A6;
end;
then reconsider F as Subset-Family of TM by XBOOLE_1:1;
reconsider F as open Subset-Family of TM by A8,TOPS_2:11;
cT c=union F
proof
let y be object;
assume
A9: y in cT;
then reconsider p=y as Point of TM;
reconsider q=y as Element of Tm by A3,A4,A9,PCOMPS_2:4;
2|^n>0 & dist(q,q)=0 by METRIC_1:1,NEWTON:83;
then
A10: q in Ball(q,1/(2|^n)) by METRIC_1:11;
reconsider BALL=Ball(q,1/(2|^n)) as Subset of TM by A3,A4,PCOMPS_2:4;
BALL in Family_open_set(Tm) by PCOMPS_1:29;
then BALL is open by A5;
then consider U be Subset of TM such that
A11: U in B and
A12: p in U and
A13: U c=BALL by A10,YELLOW_9:31;
U in F by A11,A13;
hence thesis by A12,TARSKI:def 4;
end;
then F is Cover of TM by SETFAM_1:def 11;
then consider G be Subset-Family of TM such that
A14: G c=F and
A15: G is Cover of TM & card G c=iC by A1;
take G;
let m be Nat;
assume
A16: x=m;
G is open by A14,TOPS_2:11;
hence thesis by A14,A15,A16;
end;
consider f be Function such that
A17: dom f=NAT & for e be object st e in NAT holds P[e,f.e] from CLASSES1
:sch 1(A7);
A18: union rng f c=B
proof
let b be object;
assume b in union rng f;
then consider y be set such that
A19: b in y and
A20: y in rng f by TARSKI:def 4;
consider x be object such that
A21: x in dom f and
A22: f.x=y by A20,FUNCT_1:def 3;
reconsider n=x as Nat by A17,A21;
ex G be open Subset-Family of TM st G c={U where U is Subset of TM:
U in B & ex p be Point of Tm st U c=Ball(p,1/(2|^n))} & G is Cover of TM & card
G c=iC & f.n=G by A17,A21;
then b in {U where U is Subset of TM:U in B & ex p be Point of Tm st U
c= Ball(p,1/(2|^n))} by A19,A22;
then ex U be Subset of TM st U=b & U in B & ex p be Point of Tm st U c=
Ball(p,1/(2|^n));
hence thesis;
end;
then reconsider Urngf=union rng f as Subset-Family of TM by XBOOLE_1:1;
for A be Subset of TM st A is open for p be Point of TM st p in A ex
a be Subset of TM st a in Urngf & p in a & a c=A
proof
let A be Subset of TM;
assume A is open;
then
A23: A in Family_open_set(Tm) by A5;
let p be Point of TM such that
A24: p in A;
reconsider p9=p as Element of Tm by A3,A4,PCOMPS_2:4;
consider r be Real such that
A25: r>0 and
A26: Ball(p9,r)c=A by A23,A24,PCOMPS_1:def 4;
consider n be Nat such that
A27: 1/(2|^n)<=r/2 by A25,PREPOWER:92;
A28: n in NAT by ORDINAL1:def 12;
consider G be open Subset-Family of TM such that
A29: G c={U where U is Subset of TM:U in B & ex p be Point of Tm st
U c= Ball(p,1/(2|^n))} and
A30: G is Cover of TM and
card G c=iC and
A31: f.n=G by A17,A28;
[#]TM=union G by A30,SETFAM_1:45;
then consider a be set such that
A32: p in a and
A33: a in G by A3,TARSKI:def 4;
a in {U where U is Subset of TM:U in B & ex p be Point of Tm st U
c=Ball(p,1/(2|^n))} by A29,A33;
then consider U be Subset of TM such that
A34: a=U and
U in B and
A35: ex p be Point of Tm st U c=Ball(p,1/(2|^n));
take U;
f.n in rng f by A17,FUNCT_1:def 3,A28;
hence U in Urngf & p in U by A31,A32,A33,A34,TARSKI:def 4;
thus U c=A
proof
let u9 be object;
consider pp be Element of Tm such that
A36: U c=Ball(pp,1/(2|^n)) by A35;
assume
A37: u9 in U;
then reconsider u=u9 as Element of Tm by A3,A4,PCOMPS_2:4;
dist(pp,u)<1/(2|^n) by A36,A37,METRIC_1:11;
then
A38: dist(pp,u) < r/2 by A27,XXREAL_0:2;
dist(pp,p9)<1/(2|^n) by A32,A34,A36,METRIC_1:11;
then dist(p9,pp)<r/2 by A27,XXREAL_0:2;
then
dist(p9,u)<=dist(p9,pp)+dist(pp,u) & dist(p9,pp)+dist(pp,u)<r/2+r
/2 by A38,METRIC_1:4,XREAL_1:8;
then dist(p9,u)<r/2+r/2 by XXREAL_0:2;
then u in Ball(p9,r) by METRIC_1:11;
hence thesis by A26;
end;
end;
then reconsider Urngf as Basis of TM by A6,A18,XBOOLE_1:1,YELLOW_9:32;
take Urngf;
for x be object st x in dom f holds card(f.x)c=iC
proof
let x be object;
assume x in dom f;
then reconsider n=x as Element of NAT by A17;
ex G be open Subset-Family of TM st G c={U where U is Subset of TM:
U in B & ex p be Point of Tm st U c=Ball(p,1/(2|^n))} & G is Cover of TM & card
G c=iC & f.n=G by A17;
hence thesis;
end;
then card Union f c=(omega)*`iC by A17,CARD_1:47,CARD_2:86;
hence thesis by A18,Lm5;
end;
end;
begin :: Properties of Lindel\"of spaces
definition
let T;
attr T is Lindelof means
:Def2:
for F st F is open & F is Cover of T ex G st
G c=F & G is Cover of T & G is countable;
end;
Lm8: T is Lindelof iff for F st F is open & F is Cover of T ex G st G c=F & G
is Cover of T & card G c=omega
proof
hereby
assume
A1: T is Lindelof;
let F;
assume F is open & F is Cover of T;
then consider G be Subset-Family of T such that
A2: G c=F & G is Cover of T & G is countable by A1;
take G;
thus G c=F & G is Cover of T & card G c=omega by A2;
end;
assume
A3: for F st F is open & F is Cover of T ex G st G c=F & G is Cover of T
& card G c=omega;
let F;
assume F is open & F is Cover of T;
then consider G such that
A4: G c=F & G is Cover of T and
A5: card G c=omega by A3;
G is countable by A5;
hence thesis by A4;
end;
theorem
for B be Basis of TM st TM is Lindelof ex B9 be Basis of TM st B9 c= B
& B9 is countable
proof
let B be Basis of TM;
assume TM is Lindelof;
then for F be Subset-Family of TM st F is open & F is Cover of TM ex G be
Subset-Family of TM st G c=F & G is Cover of TM & card G c=omega by Lm8;
then consider underB be Basis of TM such that
A1: underB c=B & card underB c=omega by Th23;
take underB;
thus thesis by A1;
end;
:: General Topology Cor 4.1.16 (b) <=> (a)
Lm9: TM is Lindelof iff TM is second-countable
proof
hereby
assume TM is Lindelof;
then for F be Subset-Family of TM st F is open & F is Cover of TM ex G be
Subset-Family of TM st G c=F & G is Cover of TM & card G c=omega by Lm8;
then weight TM c=omega by Th18;
hence TM is second-countable by WAYBEL23:def 6;
end;
assume TM is second-countable;
then weight TM c=omega by WAYBEL23:def 6;
then for F be Subset-Family of TM st F is open & F is Cover of TM ex G be
Subset-Family of TM st G c=F & G is Cover of TM & card G c=omega by Th18;
hence thesis by Lm8;
end;
registration
cluster Lindelof -> second-countable for metrizable TopSpace;
coherence by Lm9;
end;
:: General Topology Cor 4.1.16 (b) <=> (c)
Lm10: TM is Lindelof iff TM is separable
proof
hereby
assume TM is Lindelof;
then weight TM c=omega by WAYBEL23:def 6;
then density TM c=omega by Th22;
hence TM is separable by TOPGEN_1:def 13;
end;
assume TM is separable;
then density TM c=omega by TOPGEN_1:def 13;
then weight TM c=omega by Th22;
then TM is second-countable by WAYBEL23:def 6;
hence thesis by Lm9;
end;
registration
cluster Lindelof -> separable for metrizable TopSpace;
coherence by Lm10;
cluster separable -> Lindelof for metrizable TopSpace;
coherence by Lm10;
end;
registration
:: General Topology Th 3.8.1
cluster Lindelof metrizable for non empty TopSpace;
existence
proof
set X=the non empty finite set;
TopSpaceMetr DiscreteSpace X is finite;
hence thesis;
end;
:: General Topology Th 3.8.2
cluster second-countable -> Lindelof for TopSpace;
coherence
proof
let T be TopSpace;
assume
A1: T is second-countable;
let F be Subset-Family of T such that
A2: F is open and
A3: F is Cover of T;
per cases;
suppose
A4: T is empty;
take F;
F c={{}}
proof
let x be object;
assume x in F;
then x={} by A4;
hence thesis by TARSKI:def 1;
end;
hence thesis by A3;
end;
suppose
T is non empty;
hence thesis by A1,A2,A3,COMPL_SP:34;
end;
end;
cluster regular Lindelof -> normal for TopSpace;
coherence
proof
let T be TopSpace;
assume that
A5: T is regular and
A6: T is Lindelof;
per cases;
suppose
A7: T is empty;
let F1,F2 be Subset of T such that
F1 is closed and
F2 is closed and
A8: F1 misses F2;
take F1,F2;
thus thesis by A7,A8;
end;
suppose
A9: T is non empty;
set TOP=the topology of T;
for A be Subset of T,U be open Subset of T st A is closed & U is
open & A c= U ex W be sequence of bool(the carrier of T) st A c=Union W &
Union W c= U & for n be Element of NAT holds Cl(W.n)c=U & W.n is open
proof
let A be Subset of T,U be open Subset of T such that
A10: A is closed and
U is open and
A11: A c=U;
defpred P[object,object] means
for p be Point of T st p=$1 ex W be Subset of
T st W is open & p in W & Cl W c=U & $2=W;
A12: for x be object st x in A ex y be object st y in TOP & P[x,y]
proof
let x be object;
assume
A13: x in A;
then reconsider p=x as Point of T;
U=U``;
then consider G1,G2 be Subset of T such that
A14: G1 is open and
A15: G2 is open and
A16: p in G1 and
A17: U`c=G2 and
A18: G1 misses G2 by A5,A11,A13;
A19: Cl(G2`)=G2` & G2`c=U by A15,A17,PRE_TOPC:22,SUBSET_1:17;
take G1;
thus G1 in TOP by A14;
G1 c=G2` by A18,SUBSET_1:23;
then
A20: Cl G1 c=Cl(G2`) by PRE_TOPC:19;
let q be Point of T;
assume q=x;
hence thesis by A14,A16,A20,A19,XBOOLE_1:1;
end;
consider w be Function of A,TOP such that
A21: for x be object st x in A holds P[x,w.x] from FUNCT_2:sch 1(A12);
A` in TOP by A10,PRE_TOPC:def 2;
then TOP is open & {A`}c=TOP by ZFMISC_1:31;
then reconsider RNG=rng w,AA={A`} as open Subset-Family of T by
TOPS_2:11,XBOOLE_1:1;
set RngA=RNG\/AA;
A22: dom w=A by FUNCT_2:def 1;
[#]T c=union RngA
proof
let x be object;
assume
A23: x in [#]T;
per cases;
suppose
A24: x in A;
then consider W be Subset of T such that
W is open and
A25: x in W and
Cl W c=U and
A26: w.x=W by A21;
W in rng w by A22,A24,A26,FUNCT_1:def 3;
then W in RngA by XBOOLE_0:def 3;
hence thesis by A25,TARSKI:def 4;
end;
suppose
A27: not x in A;
A` in AA by TARSKI:def 1;
then
A28: A` in RngA by XBOOLE_0:def 3;
x in A` by A23,A27,XBOOLE_0:def 5;
hence thesis by A28,TARSKI:def 4;
end;
end;
then RngA is open Subset-Family of T & RngA is Cover of T by
SETFAM_1:def 11,TOPS_2:13;
then consider G be Subset-Family of T such that
A29: G c=RngA and
A30: G is Cover of T and
A31: G is countable by A6;
A32: [#]T=union G by A30,SETFAM_1:45;
per cases;
suppose
G\AA is empty;
then G c=AA by XBOOLE_1:37;
then
A33: union G c=union AA by ZFMISC_1:77;
take W=(NAT-->{}T);
rng W={{}T} by FUNCOP_1:8;
then
A34: ({}T)`=[#]T & Union W={}T by ZFMISC_1:25;
union AA=A` by ZFMISC_1:25;
then A`=[#]T by A32,A33;
hence A c=Union W & Union W c=U by A34,SUBSET_1:42;
let n be Element of NAT;
W.n={}T by FUNCOP_1:7;
then Cl(W.n)={}T by PRE_TOPC:22;
hence thesis by FUNCOP_1:7;
end;
suppose
A35: G\AA is non empty;
G\AA is countable by A31,CARD_3:95;
then consider W be sequence of G\AA such that
A36: rng W=G\AA by A35,CARD_3:96;
reconsider W as sequence of bool(the carrier of T) by A35,A36,
FUNCT_2:6;
take W;
thus A c=Union W
proof
let x be object;
assume
A37: x in A;
then consider y be set such that
A38: x in y and
A39: y in G by A32,TARSKI:def 4;
not x in A` by A37,XBOOLE_0:def 5;
then not y in AA by A38,TARSKI:def 1;
then y in rng W by A36,A39,XBOOLE_0:def 5;
then ex n be object st n in dom W & W.n=y by FUNCT_1:def 3;
hence thesis by A38,PROB_1:12;
end;
A40: dom W=NAT by FUNCT_2:def 1;
thus Union W c=U
proof
let x be object;
assume x in Union W;
then consider n be Nat such that
A41: x in W.n by PROB_1:12;
A42: n in NAT by ORDINAL1:def 12;
A43: W.n in G\AA by A36,A40,FUNCT_1:def 3,A42;
then W.n in G by ZFMISC_1:56;
then
A44: W.n in RNG or W.n in AA by A29,XBOOLE_0:def 3;
W.n<>A` by A43,ZFMISC_1:56;
then consider xx be object such that
A45: xx in dom w & w.xx=W.n by A44,FUNCT_1:def 3,TARSKI:def 1;
consider W9 be Subset of T such that
W9 is open and
xx in W9 and
A46: Cl W9 c=U and
A47: W.n=W9 by A21,A22,A45;
W9 c=Cl W9 by PRE_TOPC:18;
then x in Cl W9 by A41,A47;
hence thesis by A46;
end;
let n be Element of NAT;
A48: W.n in G\AA by A36,A40,FUNCT_1:def 3;
then W.n in G by ZFMISC_1:56;
then
A49: W.n in RNG or W.n in AA by A29,XBOOLE_0:def 3;
W.n<>A` by A48,ZFMISC_1:56;
then consider xx be object such that
A50: xx in dom w & w.xx=W.n by A49,FUNCT_1:def 3,TARSKI:def 1;
ex W9 be Subset of T st W9 is open & xx in W9 & Cl W9 c=U & W.n
=W9 by A21,A22,A50;
hence thesis;
end;
end;
hence thesis by A9,NAGATA_1:18;
end;
end;
cluster countable -> Lindelof for TopSpace;
coherence
proof
let T be TopSpace;
assume T is countable;
then [#]T is countable by ORDERS_4:def 2;
then
A51: card[#]T c=omega;
let F be Subset-Family of T;
assume that
F is open and
A52: F is Cover of T;
consider G be Subset-Family of T such that
A53: G c=F & G is Cover of T and
A54: card G c=card[#]T by A52,Th16;
take G;
card G c=omega by A51,A54;
hence thesis by A53;
end;
end;
Lm11: the TopStruct of TOP-REAL 1 is second-countable
proof
reconsider R=RAT as Subset of R^1 by NUMBERS:12,TOPMETR:17;
the TopStruct of TOP-REAL 1 = TopSpaceMetr Euclid 1 & the TopStruct of
TOP-REAL (1+1) = TopSpaceMetr Euclid (1+1) by EUCLID:def 8;
then
A1: weight [:the TopStruct of TOP-REAL 1, the TopStruct of TOP-REAL 1:] =
weight the TopStruct of TOP-REAL 2 by Th4,TOPREAL7:25;
Cl R=[#](R^1) by BORSUK_5:15;
then R is dense by TOPS_1:def 3;
then R^1 is separable by TOPGEN_4:6;
then
A2: weight [:R^1,R^1:] c= omega by TOPMETR:def 6,WAYBEL23:def 6;
the TopStruct of [:R^1,R^1:], the TopStruct of TOP-REAL 2
are_homeomorphic by TOPREAL6:77,TOPREALA:15;
then
A3: weight the TopStruct of [:R^1,R^1:] = weight the TopStruct of TOP-REAL 2
by Th4;
weight (the TopStruct of TOP-REAL 1) c= weight [:the TopStruct of
TOP-REAL 1,the TopStruct of TOP-REAL 1:] by Th6;
then weight (the TopStruct of TOP-REAL 1) c= omega by A1,A3,A2;
hence thesis by WAYBEL23:def 6;
end;
registration
let n be Nat;
cluster the TopStruct of TOP-REAL n -> second-countable;
coherence
proof
defpred P[Nat] means the TopStruct of TOP-REAL $1 is second-countable;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
A2: the TopStruct of TOP-REAL (n+1) = TopSpaceMetr Euclid (n+1) & n in
NAT by EUCLID:def 8,ORDINAL1:def 12;
assume P[n];
then
A3: weight [:the TopStruct of TOP-REAL n, the TopStruct of TOP-REAL 1:]
c= omega by Lm11,WAYBEL23:def 6;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n & the TopStruct
of TOP-REAL 1 = TopSpaceMetr Euclid 1 by EUCLID:def 8;
then
weight [:the TopStruct of TOP-REAL n, the TopStruct of TOP-REAL 1:]
= weight the TopStruct of TOP-REAL(n+1) by A2,Th4,TOPREAL7:25;
hence thesis by A3,WAYBEL23:def 6;
end;
[#](TOP-REAL 0) = REAL 0 by EUCLID:22
.= 0-tuples_on REAL by EUCLID:def 1
.= {<*>REAL} by FINSEQ_2:94;
then the TopStruct of TOP-REAL 0 is finite;
then
A4: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
end;
registration
let T be Lindelof TopSpace;
let A be closed Subset of T;
cluster T|A -> Lindelof;
coherence
proof
reconsider E={{}} as Subset-Family of T|A by SETFAM_1:46;
defpred P[object,object] means ex D2 being set st D2 = $2 & D2/\A=$1;
set TOP=the topology of T;
let FA be Subset-Family of T|A such that
A1: FA is open and
A2: FA is Cover of T|A;
A3: for x be object st x in FA ex y be object st y in TOP & P[x,y]
proof
let x be object such that
A4: x in FA;
reconsider X=x as Subset of T|A by A4;
X is open by A1,A4;
then X in the topology of T|A;
then consider Q be Subset of T such that
A5: Q in TOP & X=Q/\[#](T|A) by PRE_TOPC:def 4;
take Q;
thus Q in TOP by A5;
take Q;
thus thesis by A5,PRE_TOPC:def 5;
end;
consider f be Function of FA,TOP such that
A6: for x be object st x in FA holds P[x,f.x] from FUNCT_2:sch 1(A3);
A` in TOP by PRE_TOPC:def 2;
then TOP is open & {A`}c=TOP by ZFMISC_1:31;
then reconsider RNG=rng f,AA={A`} as open Subset-Family of T by TOPS_2:11
,XBOOLE_1:1;
reconsider RA=RNG\/AA as open Subset-Family of T by TOPS_2:13;
A7: A = [#](T|A) by PRE_TOPC:def 5;
A8: dom f = FA by FUNCT_2:def 1;
[#]T c=union RA
proof
A9: A\/(A`)=[#](the carrier of T) by SUBSET_1:10;
let x be object such that
A10: x in [#]T;
per cases by A9,A10,XBOOLE_0:def 3;
suppose
A11: x in A;
A=union FA by A2,A7,SETFAM_1:45;
then consider y be set such that
A12: x in y and
A13: y in FA by A11,TARSKI:def 4;
f.y in RNG by A8,A13,FUNCT_1:def 3;
then
A14: f.y in RA by XBOOLE_0:def 3;
P[y,f.y] by A6,A13;
then (f.y)/\A=y;
then x in f.y by A12,XBOOLE_0:def 4;
hence thesis by A14,TARSKI:def 4;
end;
suppose
A15: x in A`;
A` in AA by TARSKI:def 1;
then A` in RA by XBOOLE_0:def 3;
hence thesis by A15,TARSKI:def 4;
end;
end;
then RA is Cover of T by SETFAM_1:def 11;
then consider G be Subset-Family of T such that
A16: G c=RA and
A17: G is Cover of T and
A18: G is countable by Def2;
set GA=G|A;
take GE=GA\E;
thus GE c=FA
proof
let x be object;
assume
A19: x in GE;
then
A20: x<>{} by ZFMISC_1:56;
x in GA by A19,ZFMISC_1:56;
then consider R be Subset of T such that
A21: R in G and
A22: R /\ A = x by TOPS_2:def 3;
per cases by A16,A21,XBOOLE_0:def 3;
suppose
R in RNG;
then consider y be object such that
A23: y in dom f and
A24: f.y=R by FUNCT_1:def 3;
P[y,f.y] by A6,A23;
then y=R/\A by A24;
hence thesis by A22,A23;
end;
suppose
R in AA;
then R=A` by TARSKI:def 1;
then x=A\A by A22,SUBSET_1:13;
hence thesis by A20,XBOOLE_1:37;
end;
end;
union G=[#]T by A17,SETFAM_1:45;
then [#](T|A) = union GA by A7,TOPS_2:33
.= union GE by PARTIT1:2;
hence GE is Cover of T|A by SETFAM_1:def 11;
A25: card GA c=card G by Th7;
card G c=omega by A18;
then card GA c=omega by A25;
then GA is countable;
hence thesis by CARD_3:95;
end;
end;
registration
let TM be Lindelof metrizable TopSpace;
let A be Subset of TM;
:: General Topology Cor 3.8.4
cluster TM|A -> Lindelof;
coherence;
end;
definition
let T;
let A,B,L be Subset of T;
pred L separates A,B means
ex U,W be open Subset of T st A c=U & B c= W & U misses W & L=(U\/W)`;
end;
Lm12: for M be non empty MetrSpace for A,B be non empty Subset of TopSpaceMetr
M holds {p where p is Point of TopSpaceMetr M:(dist_min A).p-(dist_min B).p<0}
is open Subset of TopSpaceMetr M
proof
let M be non empty MetrSpace;
set TM=TopSpaceMetr M;
let A,B be non empty Subset of TM;
set dA=dist_min A;
set dB=dist_min B;
consider g be Function of the carrier of TM,the carrier of(R^1) such that
A1: for p be Point of TM,r1,r2 be Real st dA.p=r1 & dB.p=r2 holds
g.p=r1-r2 and
A2: g is continuous by JGRAPH_2:21;
set gA={p where p is Point of TM:dA.p-dB.p<0};
reconsider A=].-infty,0.[ as Subset of R^1 by TOPMETR:17;
A3: A is open by BORSUK_5:40;
A4: g"A c=gA
proof
let x be object;
assume
A5: x in g"A;
then reconsider p=x as Point of TM;
A6: g.x in A by A5,FUNCT_1:def 7;
dA.p-dB.p=g.x by A1;
then dA.p-dB.p<0 by A6,XXREAL_1:233;
hence thesis;
end;
A7: gA c=g"A
proof
let x be object;
assume x in gA;
then consider p be Point of TM such that
A8: p=x and
A9: dA.p-dB.p<0;
g.p=dA.p-dB.p by A1;
then dom g=[#]TM & g.p in A by A9,FUNCT_2:def 1,XXREAL_1:233;
hence thesis by A8,FUNCT_1:def 7;
end;
[#]R^1={} implies [#]TM={};
then g"A is open by A2,A3,TOPS_2:43;
hence thesis by A4,A7,XBOOLE_0:def 10;
end;
Lm13: for A,B be Subset of TM st A,B are_separated ex U,W be open Subset of TM
st A c=U & B c=W & U misses W
proof
let A,B be Subset of TM such that
A1: A,B are_separated;
set TOP=the topology of TM,cTM=the carrier of TM;
consider metr be Function of[:cTM,cTM:],REAL such that
A2: metr is_metric_of cTM and
A3: Family_open_set(SpaceMetr(cTM,metr))=TOP by PCOMPS_1:def 8;
per cases;
suppose
A4: A={}TM;
take {}TM,[#]TM;
thus thesis by A4;
end;
suppose
A5: B={}TM;
take [#]TM,{}TM;
thus thesis by A5;
end;
suppose
A6: A<>{}TM & B<>{}TM;
then
A7: TM is non empty;
then reconsider Tm=SpaceMetr(cTM,metr) as non empty MetrSpace by A2,
PCOMPS_1:36;
set TTm=TopSpaceMetr Tm;
reconsider A9=A,B9=B as Subset of TTm by A2,A7,PCOMPS_2:4;
set dA=dist_min A9,dB=dist_min B9;
reconsider U={p where p is Point of Tm:dA.p-dB.p<0}, W={p where p is Point
of Tm:dB.p-dA.p<0} as open Subset of TTm by A6,Lm12;
U in Family_open_set(Tm) & W in Family_open_set(Tm) by PRE_TOPC:def 2;
then reconsider U,W as open Subset of TM by A3,PRE_TOPC:def 2;
take U,W;
A8: [#]TM=[#]TTm by A2,A7,PCOMPS_2:4;
thus A c=U
proof
let x be object;
assume
A9: x in A;
then reconsider p=x as Point of Tm by A2,A7,PCOMPS_2:4;
A misses Cl B by A1,CONNSP_1:def 1;
then not x in Cl B by A9,XBOOLE_0:3;
then not x in Cl B9 by A3,A8,TOPS_3:80;
then
A10: dB.p<>0 by A6,HAUSDORF:8;
A11: dB.p>=0 by A6,JORDAN1K:9;
dA.p=0 by A9,HAUSDORF:5;
then dA.p-dB.p<0 by A10,A11;
hence thesis;
end;
thus B c=W
proof
let x be object;
assume
A12: x in B;
then reconsider p=x as Point of Tm by A2,A7,PCOMPS_2:4;
B misses Cl A by A1,CONNSP_1:def 1;
then not x in Cl A by A12,XBOOLE_0:3;
then not x in Cl A9 by A3,A8,TOPS_3:80;
then
A13: dA.p<>0 by A6,HAUSDORF:8;
A14: dA.p>=0 by A6,JORDAN1K:9;
dB.p=0 by A12,HAUSDORF:5;
then dB.p-dA.p<0 by A13,A14;
hence thesis;
end;
thus U misses W
proof
assume U meets W;
then consider x be object such that
A15: x in U and
A16: x in W by XBOOLE_0:3;
consider p be Point of Tm such that
A17: p=x and
A18: dB.p-dA.p<0 by A16;
ex q be Point of Tm st q=x & dA.q-dB.q<0 by A15;
then -(dA.p-dB.p)>-0 by A17;
hence thesis by A18;
end;
end;
end;
:: Teoria wymiaru Lm 1.2.8
theorem
Am,Bm are_separated implies ex L be Subset of TM st L separates Am,Bm
proof
assume Am,Bm are_separated;
then consider U,W be open Subset of TM such that
A1: Am c=U & Bm c=W & U misses W by Lm13;
take (U\/W)`;
thus thesis by A1;
end;
:: Teoria wymiaru Lm 1.2.9
theorem
for M be Subset of TM, A1,A2 be closed Subset of TM, V1,V2 be open
Subset of TM st A1 c=V1 & A2 c=V2 & Cl V1 misses Cl V2 for mV1,mV2,mL be Subset
of TM|M st mV1 = M/\Cl V1 & mV2 = M/\Cl V2 & mL separates mV1,mV2 ex L be
Subset of TM st L separates A1,A2 & M/\L c= mL
proof
let M be Subset of TM,A1,A2 be closed Subset of TM,V1,V2 be open Subset of
TM such that
A1: A1 c=V1 and
A2: A2 c=V2 and
A3: Cl V1 misses Cl V2;
set TMM=TM|M;
let mV1,mV2,mL be Subset of TMM such that
A4: mV1=M/\Cl V1 and
A5: mV2=M/\Cl V2 and
A6: mL separates mV1,mV2;
A7: V2/\M c=mV2 by A5,PRE_TOPC:18,XBOOLE_1:26;
consider U9,W9 be open Subset of TMM such that
A8: mV1 c=U9 and
A9: mV2 c=W9 and
A10: U9 misses W9 and
A11: mL=(U9\/W9)` by A6;
A12: [#]TMM=M by PRE_TOPC:def 5;
then reconsider u=U9,w=W9 as Subset of TM by XBOOLE_1:1;
set u1=u\/A1,w1=w\/A2;
A13: mV2/\u c=U9/\W9 by A9,XBOOLE_1:26;
U9,W9 are_separated by A10,TSEP_1:37;
then
A14: u,w are_separated by CONNSP_1:5;
V2/\u = V2/\(M/\u) by A12,XBOOLE_1:28
.= V2/\M/\u by XBOOLE_1:16;
then V2/\u c=mV2/\u by A7,XBOOLE_1:26;
then V2/\u c=U9/\W9 by A13;
then V2/\u c={} by A10;
then V2/\u={};
then V2 misses u;
then
A15: V2 misses Cl u by TSEP_1:36;
A16: Cl u1 misses w1
proof
assume Cl u1 meets w1;
then consider x be object such that
A17: x in Cl u1 & x in w1 by XBOOLE_0:3;
A18: Cl u1=(Cl u)\/Cl A1 by PRE_TOPC:20;
per cases by A17,A18,XBOOLE_0:def 3;
suppose
x in Cl u & x in w;
then w meets Cl u by XBOOLE_0:3;
hence contradiction by A14,CONNSP_1:def 1;
end;
suppose
x in Cl u & x in A2;
hence contradiction by A2,A15,XBOOLE_0:3;
end;
suppose
A19: x in Cl A1 & x in w;
Cl A1 c=Cl V1 by A1,PRE_TOPC:19;
then x in mV1 by A4,A12,A19,XBOOLE_0:def 4;
hence contradiction by A8,A10,A19,XBOOLE_0:3;
end;
suppose
A20: x in Cl A1 & x in A2;
A21: Cl A1 c=Cl V1 & V2 c=Cl V2 by A1,PRE_TOPC:18,19;
x in V2 by A2,A20;
hence thesis by A3,A20,A21,XBOOLE_0:3;
end;
end;
A22: V1/\M c=mV1 by A4,PRE_TOPC:18,XBOOLE_1:26;
A23: mV1/\w c=U9/\W9 by A8,XBOOLE_1:26;
V1/\w = V1/\(M/\w) by A12,XBOOLE_1:28
.= V1/\M/\w by XBOOLE_1:16;
then V1/\w c=mV1/\w by A22,XBOOLE_1:26;
then V1/\w c=U9/\W9 by A23;
then V1/\w c={} by A10;
then V1/\w={};
then V1 misses w;
then
A24: V1 misses Cl w by TSEP_1:36;
Cl w1 misses u1
proof
assume Cl w1 meets u1;
then consider x be object such that
A25: x in Cl w1 & x in u1 by XBOOLE_0:3;
A26: Cl w1=(Cl w)\/Cl A2 by PRE_TOPC:20;
per cases by A25,A26,XBOOLE_0:def 3;
suppose
x in Cl w & x in u;
then Cl w meets u by XBOOLE_0:3;
hence contradiction by A14,CONNSP_1:def 1;
end;
suppose
x in Cl w & x in A1;
hence contradiction by A1,A24,XBOOLE_0:3;
end;
suppose
A27: x in Cl A2 & x in u;
Cl A2 c=Cl V2 by A2,PRE_TOPC:19;
then x in mV2 by A5,A12,A27,XBOOLE_0:def 4;
hence contradiction by A9,A10,A27,XBOOLE_0:3;
end;
suppose
A28: x in Cl A2 & x in A1;
A29: Cl A2 c=Cl V2 & V1 c=Cl V1 by A2,PRE_TOPC:18,19;
x in V1 by A1,A28;
hence thesis by A3,A28,A29,XBOOLE_0:3;
end;
end;
then u1,w1 are_separated by A16,CONNSP_1:def 1;
then consider U1,W1 be open Subset of TM such that
A30: u1 c=U1 and
A31: w1 c=W1 and
A32: U1 misses W1 by Lm13;
take L=(U1\/W1)`;
A2 c=w1 by XBOOLE_1:7;
then
A33: A2 c=W1 by A31;
w c=w1 by XBOOLE_1:7;
then
A34: w c=W1 by A31;
u c=u1 by XBOOLE_1:7;
then u c=U1 by A30;
then
A35: u\/w c=U1\/W1 by A34,XBOOLE_1:13;
A1 c=u1 by XBOOLE_1:7;
then A1 c=U1 by A30;
hence L separates A1,A2 by A32,A33;
A36: ([#]TMM)\(U9\/W9) = mL by A11;
M/\L = (M/\[#]TM)\(U1\/W1) by XBOOLE_1:49
.= M\(U1\/W1) by XBOOLE_1:28;
then M/\L c=M\(U9\/W9) by A35,XBOOLE_1:34;
hence thesis by A36,PRE_TOPC:def 5;
end;