let T be non empty TopSpace; :: thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite )

assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite

then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that

A2: metr is_metric_of the carrier of T and

A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T ;

set PM = SpaceMetr ( the carrier of T,metr);

reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;

deffunc H_{1}( Element of NAT ) -> set = { (Ball (x,(1 / (2 |^ $1)))) where x is Element of PM : x is Element of PM } ;

defpred S_{1}[ Element of NAT , set ] means $2 = H_{1}($1);

A4: for k being Element of NAT ex y being Subset-Family of T st S_{1}[k,y]

A5: for k being Element of NAT holds S_{1}[k,FB . k]
from FUNCT_2:sch 3(A4);

defpred S_{2}[ object , object ] means ex W being Subset-Family of T st

( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite );

set TPM = TopSpaceMetr PM;

A6: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;

A7: for n being Element of NAT ex PP being Subset-Family of T st

( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )

ex y being object st

( y in bool (bool the carrier of T) & S_{2}[k,y] )

A11: for x being object st x in NAT holds

S_{2}[x,UC . x]
from FUNCT_2:sch 1(A10);

A12: for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UC & p in B & B c= A )

Union UC c= the topology of T

then UC is Basis_sigma_locally_finite by A26;

hence ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ; :: thesis: verum

assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite

then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that

A2: metr is_metric_of the carrier of T and

A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T ;

set PM = SpaceMetr ( the carrier of T,metr);

reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;

deffunc H

defpred S

A4: for k being Element of NAT ex y being Subset-Family of T st S

proof

consider FB being sequence of (bool (bool the carrier of T)) such that
let k be Element of NAT ; :: thesis: ex y being Subset-Family of T st S_{1}[k,y]

set Ak = H_{1}(k);

H_{1}(k) c= bool the carrier of T
_{1}[k,y]
; :: thesis: verum

end;set Ak = H

H

proof

hence
ex y being Subset-Family of T st S
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in H_{1}(k) or B in bool the carrier of T )

assume B in H_{1}(k)
; :: thesis: B in bool the carrier of T

then ex x being Element of PM st

( B = Ball (x,(1 / (2 |^ k))) & x is Element of PM ) ;

then B in Family_open_set PM by PCOMPS_1:29;

hence B in bool the carrier of T by A3; :: thesis: verum

end;assume B in H

then ex x being Element of PM st

( B = Ball (x,(1 / (2 |^ k))) & x is Element of PM ) ;

then B in Family_open_set PM by PCOMPS_1:29;

hence B in bool the carrier of T by A3; :: thesis: verum

A5: for k being Element of NAT holds S

defpred S

( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite );

set TPM = TopSpaceMetr PM;

A6: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;

A7: for n being Element of NAT ex PP being Subset-Family of T st

( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )

proof

A10:
for k being object st k in NAT holds
let n be Element of NAT ; :: thesis: ex PP being Subset-Family of T st

( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )

[#] (TopSpaceMetr PM) c= union (FB . n)

for U being Subset of T st U in FB . n holds

U is open

then ex PP being Subset-Family of T st

( PP is open & PP is Cover of T & PP is_finer_than FB . n & PP is locally_finite ) by A1, A9, PCOMPS_2:6;

hence ex PP being Subset-Family of T st

( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) ; :: thesis: verum

end;( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )

[#] (TopSpaceMetr PM) c= union (FB . n)

proof

then A9:
FB . n is Cover of T
by A6, SETFAM_1:def 11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (TopSpaceMetr PM) or x in union (FB . n) )

assume x in [#] (TopSpaceMetr PM) ; :: thesis: x in union (FB . n)

then reconsider x9 = x as Element of PM ;

( dist (x9,x9) = 0 & 2 |^ n > 0 ) by METRIC_1:1, NEWTON:83;

then dist (x9,x9) < 1 / (2 |^ n) by XREAL_1:139;

then A8: x9 in Ball (x9,(1 / (2 |^ n))) by METRIC_1:11;

Ball (x9,(1 / (2 |^ n))) in H_{1}(n)
;

then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;

hence x in union (FB . n) by A8, TARSKI:def 4; :: thesis: verum

end;assume x in [#] (TopSpaceMetr PM) ; :: thesis: x in union (FB . n)

then reconsider x9 = x as Element of PM ;

( dist (x9,x9) = 0 & 2 |^ n > 0 ) by METRIC_1:1, NEWTON:83;

then dist (x9,x9) < 1 / (2 |^ n) by XREAL_1:139;

then A8: x9 in Ball (x9,(1 / (2 |^ n))) by METRIC_1:11;

Ball (x9,(1 / (2 |^ n))) in H

then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;

hence x in union (FB . n) by A8, TARSKI:def 4; :: thesis: verum

for U being Subset of T st U in FB . n holds

U is open

proof

then
FB . n is open
by TOPS_2:def 1;
let U be Subset of T; :: thesis: ( U in FB . n implies U is open )

assume U in FB . n ; :: thesis: U is open

then U in H_{1}(n)
by A5;

then ex x being Element of PM st

( U = Ball (x,(1 / (2 |^ n))) & x is Element of PM ) ;

then U in the topology of T by A3, PCOMPS_1:29;

hence U is open by PRE_TOPC:def 2; :: thesis: verum

end;assume U in FB . n ; :: thesis: U is open

then U in H

then ex x being Element of PM st

( U = Ball (x,(1 / (2 |^ n))) & x is Element of PM ) ;

then U in the topology of T by A3, PCOMPS_1:29;

hence U is open by PRE_TOPC:def 2; :: thesis: verum

then ex PP being Subset-Family of T st

( PP is open & PP is Cover of T & PP is_finer_than FB . n & PP is locally_finite ) by A1, A9, PCOMPS_2:6;

hence ex PP being Subset-Family of T st

( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) ; :: thesis: verum

ex y being object st

( y in bool (bool the carrier of T) & S

proof

consider UC being FamilySequence of T such that
let k be object ; :: thesis: ( k in NAT implies ex y being object st

( y in bool (bool the carrier of T) & S_{2}[k,y] ) )

assume k in NAT ; :: thesis: ex y being object st

( y in bool (bool the carrier of T) & S_{2}[k,y] )

then reconsider k = k as Element of NAT ;

ex PP being Subset-Family of T st

( PP is_finer_than FB . k & PP is Cover of T & PP is open & PP is locally_finite ) by A7;

hence ex y being object st

( y in bool (bool the carrier of T) & S_{2}[k,y] )
; :: thesis: verum

end;( y in bool (bool the carrier of T) & S

assume k in NAT ; :: thesis: ex y being object st

( y in bool (bool the carrier of T) & S

then reconsider k = k as Element of NAT ;

ex PP being Subset-Family of T st

( PP is_finer_than FB . k & PP is Cover of T & PP is open & PP is locally_finite ) by A7;

hence ex y being object st

( y in bool (bool the carrier of T) & S

A11: for x being object st x in NAT holds

S

A12: for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UC & p in B & B c= A )

proof

for n being Element of NAT holds UC . n is locally_finite
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UC & p in B & B c= A ) )

assume A is open ; :: thesis: for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UC & p in B & B c= A )

then A13: A in Family_open_set PM by A3, PRE_TOPC:def 2;

let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st

( B in Union UC & p in B & B c= A ) )

assume A14: p in A ; :: thesis: ex B being Subset of T st

( B in Union UC & p in B & B c= A )

then reconsider p = p as Element of PM by A13;

consider r1 being Real such that

A15: r1 > 0 and

A16: Ball (p,r1) c= A by A14, A13, PCOMPS_1:def 4;

consider n being Nat such that

A17: 1 / (2 |^ n) <= r1 by A15, PREPOWER:92;

A18: S_{2}[n + 1,UC . (n + 1)]
by A11;

then union (UC . (n + 1)) = the carrier of T by SETFAM_1:45;

then consider B being set such that

A19: p in B and

A20: B in UC . (n + 1) by TARSKI:def 4;

reconsider B = B as Subset of PM by A2, A20, PCOMPS_2:4;

consider B1 being set such that

A21: B1 in FB . (n + 1) and

A22: B c= B1 by A18, A20, SETFAM_1:def 2;

B1 in H_{1}(n + 1)
by A5, A21;

then consider q being Element of PM such that

A23: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and

q is Element of PM ;

A24: dist (q,p) < 1 / (2 |^ (n + 1)) by A19, A22, A23, METRIC_1:11;

B in Union UC by A20, PROB_1:12;

hence ex B being Subset of T st

( B in Union UC & p in B & B c= A ) by A16, A19, A25, XBOOLE_1:1; :: thesis: verum

end;ex B being Subset of T st

( B in Union UC & p in B & B c= A ) )

assume A is open ; :: thesis: for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UC & p in B & B c= A )

then A13: A in Family_open_set PM by A3, PRE_TOPC:def 2;

let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st

( B in Union UC & p in B & B c= A ) )

assume A14: p in A ; :: thesis: ex B being Subset of T st

( B in Union UC & p in B & B c= A )

then reconsider p = p as Element of PM by A13;

consider r1 being Real such that

A15: r1 > 0 and

A16: Ball (p,r1) c= A by A14, A13, PCOMPS_1:def 4;

consider n being Nat such that

A17: 1 / (2 |^ n) <= r1 by A15, PREPOWER:92;

A18: S

then union (UC . (n + 1)) = the carrier of T by SETFAM_1:45;

then consider B being set such that

A19: p in B and

A20: B in UC . (n + 1) by TARSKI:def 4;

reconsider B = B as Subset of PM by A2, A20, PCOMPS_2:4;

consider B1 being set such that

A21: B1 in FB . (n + 1) and

A22: B c= B1 by A18, A20, SETFAM_1:def 2;

B1 in H

then consider q being Element of PM such that

A23: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and

q is Element of PM ;

A24: dist (q,p) < 1 / (2 |^ (n + 1)) by A19, A22, A23, METRIC_1:11;

now :: thesis: for r being Element of PM st r in B holds

r in Ball (p,r1)

then A25:
B c= Ball (p,r1)
;r in Ball (p,r1)

let r be Element of PM; :: thesis: ( r in B implies r in Ball (p,r1) )

assume r in B ; :: thesis: r in Ball (p,r1)

then dist (q,r) < 1 / (2 |^ (n + 1)) by A22, A23, METRIC_1:11;

then ( dist (p,r) <= (dist (q,p)) + (dist (q,r)) & (dist (q,p)) + (dist (q,r)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A24, METRIC_1:4, XREAL_1:8;

then dist (p,r) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;

then dist (p,r) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;

then dist (p,r) < 1 / (2 |^ n) by XCMPLX_1:92;

then dist (p,r) < r1 by A17, XXREAL_0:2;

hence r in Ball (p,r1) by METRIC_1:11; :: thesis: verum

end;assume r in B ; :: thesis: r in Ball (p,r1)

then dist (q,r) < 1 / (2 |^ (n + 1)) by A22, A23, METRIC_1:11;

then ( dist (p,r) <= (dist (q,p)) + (dist (q,r)) & (dist (q,p)) + (dist (q,r)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A24, METRIC_1:4, XREAL_1:8;

then dist (p,r) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;

then dist (p,r) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;

then dist (p,r) < 1 / (2 |^ n) by XCMPLX_1:92;

then dist (p,r) < r1 by A17, XXREAL_0:2;

hence r in Ball (p,r1) by METRIC_1:11; :: thesis: verum

B in Union UC by A20, PROB_1:12;

hence ex B being Subset of T st

( B in Union UC & p in B & B c= A ) by A16, A19, A25, XBOOLE_1:1; :: thesis: verum

proof

then A26:
UC is sigma_locally_finite
;
let n be Element of NAT ; :: thesis: UC . n is locally_finite

S_{2}[n,UC . n]
by A11;

hence UC . n is locally_finite ; :: thesis: verum

end;S

hence UC . n is locally_finite ; :: thesis: verum

Union UC c= the topology of T

proof

then
Union UC is Basis of T
by A12, YELLOW_9:32;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union UC or u in the topology of T )

assume u in Union UC ; :: thesis: u in the topology of T

then consider k being Nat such that

A27: u in UC . k by PROB_1:12;

A28: k in NAT by ORDINAL1:def 12;

reconsider u9 = u as Subset of T by A27;

S_{2}[k,UC . k]
by A11, A28;

then u9 is open by A27, TOPS_2:def 1;

hence u in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;assume u in Union UC ; :: thesis: u in the topology of T

then consider k being Nat such that

A27: u in UC . k by PROB_1:12;

A28: k in NAT by ORDINAL1:def 12;

reconsider u9 = u as Subset of T by A27;

S

then u9 is open by A27, TOPS_2:def 1;

hence u in the topology of T by PRE_TOPC:def 2; :: thesis: verum

then UC is Basis_sigma_locally_finite by A26;

hence ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ; :: thesis: verum