:: NAGATA_2 semantic presentation
begin
theorem Th1: :: NAGATA_2:1
for i being Element of NAT st i > 0 holds
ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1)
proof
defpred S1[ Element of NAT ] means for k being Element of NAT st 1 <= k & k <= $1 holds
ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1);
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; ::_thesis: S1[i + 1]
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= i + 1 implies ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) )
assume that
A3: 1 <= k and
A4: k <= i + 1 ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
now__::_thesis:_ex_n,_m_being_Element_of_NAT_st_k_=_(2_|^_n)_*_((2_*_m)_+_1)
percases ( ( k = i + 1 & i = 0 ) or ( k = i + 1 & i > 0 ) or k < i + 1 ) by A4, XXREAL_0:1;
supposeA5: ( k = i + 1 & i = 0 ) ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
set m = 0 ;
A6: 1 = 2 |^ 0 by NEWTON:4;
k = 1 * ((0 * 2) + 1) by A5;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) by A6; ::_thesis: verum
end;
supposeA7: ( k = i + 1 & i > 0 ) ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
percases ( k mod 2 = 1 or k mod 2 = 0 ) by NAT_D:12;
suppose k mod 2 = 1 ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
then consider m being Nat such that
A8: k = (2 * m) + 1 and
1 < 2 by NAT_D:def_2;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
1 = 2 |^ 0 by NEWTON:4;
then k = (2 |^ 0) * ((2 * m) + 1) by A8;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; ::_thesis: verum
end;
suppose k mod 2 = 0 ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
then consider j being Nat such that
A9: k = (2 * j) + 0 and
0 < 2 by NAT_D:def_2;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A10: j <= i
proof
assume j > i ; ::_thesis: contradiction
then j + j > i + 1 by NAT_1:14, XREAL_1:8;
hence contradiction by A7, A9; ::_thesis: verum
end;
j <> 0 by A7, A9;
then j >= 1 by NAT_1:14;
then consider n, m being Element of NAT such that
A11: j = (2 |^ n) * ((2 * m) + 1) by A2, A10;
k = (2 * (2 |^ n)) * ((2 * m) + 1) by A9, A11;
then k = (2 |^ (n + 1)) * ((2 * m) + 1) by NEWTON:6;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; ::_thesis: verum
end;
end;
end;
suppose k < i + 1 ; ::_thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)
then k <= i by NAT_1:13;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) by A2, A3; ::_thesis: verum
end;
end;
end;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; ::_thesis: verum
end;
let i be Element of NAT ; ::_thesis: ( i > 0 implies ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1) )
assume i > 0 ; ::_thesis: ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1)
then A12: i >= 1 by NAT_1:14;
A13: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1);
hence ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1) by A12; ::_thesis: verum
end;
definition
func PairFunc -> Function of [:NAT,NAT:],NAT means :Def1: :: NAGATA_2:def 1
for n, m being Element of NAT holds it . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1;
existence
ex b1 being Function of [:NAT,NAT:],NAT st
for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
proof
deffunc H1( Element of NAT , Element of NAT ) -> Element of NAT = In ((((2 |^ $1) * ((2 * $2) + 1)) - 1),NAT);
A1: for n, m being Element of NAT holds ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT
proof
let n, m be Element of NAT ; ::_thesis: ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT
0 < 2 |^ n by NEWTON:83;
then ((2 |^ n) * ((2 * m) + 1)) - 1 is Element of NAT by NAT_1:20, XREAL_1:129;
hence ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT ; ::_thesis: verum
end;
consider NN being Function of [:NAT,NAT:],NAT such that
A2: for n, m being Element of NAT holds NN . (n,m) = H1(n,m) from BINOP_1:sch_4();
take NN ; ::_thesis: for n, m being Element of NAT holds NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
let n, m be Element of NAT ; ::_thesis: NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
NN . (n,m) = In ((((2 |^ n) * ((2 * m) + 1)) - 1),NAT) by A2
.= ((2 |^ n) * ((2 * m) + 1)) - 1 by A1, FUNCT_7:def_1 ;
hence NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:NAT,NAT:],NAT st ( for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds b2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds
b1 = b2
proof
let N1, N2 be Function of [:NAT,NAT:],NAT; ::_thesis: ( ( for n, m being Element of NAT holds N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds N2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) implies N1 = N2 )
assume that
A3: for n, m being Element of NAT holds N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 and
A4: for n, m being Element of NAT holds N2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ; ::_thesis: N1 = N2
now__::_thesis:_for_n,_m_being_Element_of_NAT_holds_N1_._(n,m)_=_N2_._(n,m)
let n, m be Element of NAT ; ::_thesis: N1 . (n,m) = N2 . (n,m)
N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 by A3;
hence N1 . (n,m) = N2 . (n,m) by A4; ::_thesis: verum
end;
hence N1 = N2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines PairFunc NAGATA_2:def_1_:_
for b1 being Function of [:NAT,NAT:],NAT holds
( b1 = PairFunc iff for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );
theorem Th2: :: NAGATA_2:2
PairFunc is bijective
proof
now__::_thesis:_for_nm1,_nm2_being_set_st_nm1_in_[:NAT,NAT:]_&_nm2_in_[:NAT,NAT:]_&_PairFunc_._nm1_=_PairFunc_._nm2_holds_
nm1_=_nm2
let nm1, nm2 be set ; ::_thesis: ( nm1 in [:NAT,NAT:] & nm2 in [:NAT,NAT:] & PairFunc . nm1 = PairFunc . nm2 implies nm1 = nm2 )
assume that
A1: nm1 in [:NAT,NAT:] and
A2: nm2 in [:NAT,NAT:] and
A3: PairFunc . nm1 = PairFunc . nm2 ; ::_thesis: nm1 = nm2
consider n2, m2 being set such that
A4: ( n2 in NAT & m2 in NAT ) and
A5: [n2,m2] = nm2 by A2, ZFMISC_1:def_2;
consider n1, m1 being set such that
A6: ( n1 in NAT & m1 in NAT ) and
A7: [n1,m1] = nm1 by A1, ZFMISC_1:def_2;
reconsider n1 = n1, n2 = n2, m1 = m1, m2 = m2 as Element of NAT by A6, A4;
A8: ((2 |^ n2) * ((2 * m2) + 1)) - 1 = PairFunc . nm2 by A5, Def1;
A9: ((2 |^ n1) * ((2 * m1) + 1)) - 1 = PairFunc . nm1 by A7, Def1;
then n1 = n2 by A3, A8, CARD_4:4;
hence nm1 = nm2 by A3, A7, A5, A9, A8, CARD_4:4; ::_thesis: verum
end;
hence PairFunc is one-to-one by FUNCT_2:19; :: according to FUNCT_2:def_4 ::_thesis: PairFunc is onto
now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
i_in_rng_PairFunc
let i be set ; ::_thesis: ( i in NAT implies i in rng PairFunc )
assume i in NAT ; ::_thesis: i in rng PairFunc
then reconsider i9 = i as Element of NAT ;
consider n, m being Element of NAT such that
A10: i9 + 1 = (2 |^ n) * ((2 * m) + 1) by Th1;
i9 - 0 = ((2 |^ n) * ((2 * m) + 1)) - 1 by A10;
then ( dom PairFunc = [:NAT,NAT:] & i = PairFunc . [n,m] ) by Def1, FUNCT_2:def_1;
hence i in rng PairFunc by FUNCT_1:def_3; ::_thesis: verum
end;
then NAT c= rng PairFunc by TARSKI:def_3;
then NAT = rng PairFunc by XBOOLE_0:def_10;
hence PairFunc is onto by FUNCT_2:def_3; ::_thesis: verum
end;
definition
let X be set ;
let f be Function of [:X,X:],REAL;
let x be Element of X;
func dist (f,x) -> Function of X,REAL means :Def2: :: NAGATA_2:def 2
for y being Element of X holds it . y = f . (x,y);
existence
ex b1 being Function of X,REAL st
for y being Element of X holds b1 . y = f . (x,y)
proof
deffunc H1( set ) -> set = f . (x,$1);
A1: for y being set st y in X holds
H1(y) in REAL
proof
let y be set ; ::_thesis: ( y in X implies H1(y) in REAL )
assume y in X ; ::_thesis: H1(y) in REAL
f . [x,y] in REAL ;
hence H1(y) in REAL ; ::_thesis: verum
end;
consider DIST being Function of X,REAL such that
A2: for y being set st y in X holds
DIST . y = H1(y) from FUNCT_2:sch_2(A1);
now__::_thesis:_for_y_being_Element_of_X_holds_f_._(x,y)_=_DIST_._y
percases ( X is empty or not X is empty ) ;
supposeA3: X is empty ; ::_thesis: for y being Element of X holds f . (x,y) = DIST . y
let y be Element of X; ::_thesis: f . (x,y) = DIST . y
not [x,y] in dom f by A3;
then A4: f . [x,y] = {} by FUNCT_1:def_2;
not y in dom DIST by A3;
hence f . (x,y) = DIST . y by A4, FUNCT_1:def_2; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: for y being Element of X holds DIST . y = f . (x,y)
hence for y being Element of X holds DIST . y = f . (x,y) by A2; ::_thesis: verum
end;
end;
end;
hence ex b1 being Function of X,REAL st
for y being Element of X holds b1 . y = f . (x,y) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of X,REAL st ( for y being Element of X holds b1 . y = f . (x,y) ) & ( for y being Element of X holds b2 . y = f . (x,y) ) holds
b1 = b2
proof
let D1, D2 be Function of X,REAL; ::_thesis: ( ( for y being Element of X holds D1 . y = f . (x,y) ) & ( for y being Element of X holds D2 . y = f . (x,y) ) implies D1 = D2 )
assume that
A5: for y being Element of X holds D1 . y = f . (x,y) and
A6: for y being Element of X holds D2 . y = f . (x,y) ; ::_thesis: D1 = D2
now__::_thesis:_for_y_being_Element_of_X_holds_D1_._y_=_D2_._y
let y be Element of X; ::_thesis: D1 . y = D2 . y
D1 . y = f . (x,y) by A5;
hence D1 . y = D2 . y by A6; ::_thesis: verum
end;
hence D1 = D2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines dist NAGATA_2:def_2_:_
for X being set
for f being Function of [:X,X:],REAL
for x being Element of X
for b4 being Function of X,REAL holds
( b4 = dist (f,x) iff for y being Element of X holds b4 . y = f . (x,y) );
theorem Th3: :: NAGATA_2:3
for T1, T2 being non empty TopSpace
for D being Subset of [:T1,T2:] st D is open holds
for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
proof
let T1, T2 be non empty TopSpace; ::_thesis: for D being Subset of [:T1,T2:] st D is open holds
for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
let D be Subset of [:T1,T2:]; ::_thesis: ( D is open implies for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) ) )
assume D is open ; ::_thesis: for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
then consider FA being Subset-Family of [:T1,T2:] such that
A1: D = union FA and
A2: for B being set st B in FA holds
ex B1 being Subset of T1 ex B2 being Subset of T2 st
( B = [:B1,B2:] & B1 is open & B2 is open ) by BORSUK_1:5;
let x1 be Point of T1; ::_thesis: for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
let x2 be Point of T2; ::_thesis: for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
let X1 be Subset of T1; ::_thesis: for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
let X2 be Subset of T2; ::_thesis: ( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
thus ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) ::_thesis: ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open )
proof
assume A3: X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) ; ::_thesis: X1 is open
for t being set holds
( t in X1 iff ex U being Subset of T1 st
( U is open & U c= X1 & t in U ) )
proof
let t be set ; ::_thesis: ( t in X1 iff ex U being Subset of T1 st
( U is open & U c= X1 & t in U ) )
( t in X1 implies ex U being Subset of T1 st
( U is open & U c= X1 & t in U ) )
proof
assume t in X1 ; ::_thesis: ex U being Subset of T1 st
( U is open & U c= X1 & t in U )
then consider tx being set such that
A4: tx in dom (pr1 ( the carrier of T1, the carrier of T2)) and
A5: tx in D /\ [: the carrier of T1,{x2}:] and
A6: t = (pr1 ( the carrier of T1, the carrier of T2)) . tx by A3, FUNCT_1:def_6;
tx in D by A5, XBOOLE_0:def_4;
then consider tX being set such that
A7: tx in tX and
A8: tX in FA by A1, TARSKI:def_4;
consider tX1 being Subset of T1, tX2 being Subset of T2 such that
A9: tX = [:tX1,tX2:] and
A10: tX1 is open and
tX2 is open by A2, A8;
take tX1 ; ::_thesis: ( tX1 is open & tX1 c= X1 & t in tX1 )
thus tX1 is open by A10; ::_thesis: ( tX1 c= X1 & t in tX1 )
consider tx1, tx2 being set such that
A11: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and
A12: tx = [tx1,tx2] by A4, ZFMISC_1:def_2;
thus tX1 c= X1 ::_thesis: t in tX1
proof
tx in [: the carrier of T1,{x2}:] by A5, XBOOLE_0:def_4;
then A13: tx2 = x2 by A12, ZFMISC_1:106;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in tX1 or a in X1 )
assume A14: a in tX1 ; ::_thesis: a in X1
[a,x2] in [: the carrier of T1, the carrier of T2:] by A14, ZFMISC_1:87;
then A15: [a,x2] in dom (pr1 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def_4;
tx2 in tX2 by A12, A7, A9, ZFMISC_1:87;
then [a,x2] in [:tX1,tX2:] by A14, A13, ZFMISC_1:87;
then A16: [a,x2] in union FA by A8, A9, TARSKI:def_4;
[a,x2] in [: the carrier of T1,{x2}:] by A14, ZFMISC_1:106;
then [a,x2] in D /\ [: the carrier of T1,{x2}:] by A1, A16, XBOOLE_0:def_4;
then (pr1 ( the carrier of T1, the carrier of T2)) . (a,x2) in (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) by A15, FUNCT_1:def_6;
hence a in X1 by A3, A14, FUNCT_3:def_4; ::_thesis: verum
end;
(pr1 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx1 by A11, FUNCT_3:def_4;
hence t in tX1 by A6, A12, A7, A9, ZFMISC_1:87; ::_thesis: verum
end;
hence ( t in X1 iff ex U being Subset of T1 st
( U is open & U c= X1 & t in U ) ) ; ::_thesis: verum
end;
hence X1 is open by TOPS_1:25; ::_thesis: verum
end;
thus ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) ::_thesis: verum
proof
assume A17: X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) ; ::_thesis: X2 is open
for t being set holds
( t in X2 iff ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) )
proof
let t be set ; ::_thesis: ( t in X2 iff ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) )
( t in X2 implies ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) )
proof
assume t in X2 ; ::_thesis: ex U being Subset of T2 st
( U is open & U c= X2 & t in U )
then consider tx being set such that
A18: tx in dom (pr2 ( the carrier of T1, the carrier of T2)) and
A19: tx in D /\ [:{x1}, the carrier of T2:] and
A20: t = (pr2 ( the carrier of T1, the carrier of T2)) . tx by A17, FUNCT_1:def_6;
tx in D by A19, XBOOLE_0:def_4;
then consider tX being set such that
A21: tx in tX and
A22: tX in FA by A1, TARSKI:def_4;
consider tx1, tx2 being set such that
A23: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and
A24: tx = [tx1,tx2] by A18, ZFMISC_1:def_2;
A25: (pr2 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx2 by A23, FUNCT_3:def_5;
consider tX1 being Subset of T1, tX2 being Subset of T2 such that
A26: tX = [:tX1,tX2:] and
tX1 is open and
A27: tX2 is open by A2, A22;
A28: tX2 c= X2
proof
tx in [:{x1}, the carrier of T2:] by A19, XBOOLE_0:def_4;
then A29: tx1 = x1 by A24, ZFMISC_1:105;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in tX2 or a in X2 )
assume A30: a in tX2 ; ::_thesis: a in X2
[x1,a] in [: the carrier of T1, the carrier of T2:] by A30, ZFMISC_1:87;
then A31: [x1,a] in dom (pr2 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def_5;
tx1 in tX1 by A24, A21, A26, ZFMISC_1:87;
then [x1,a] in [:tX1,tX2:] by A30, A29, ZFMISC_1:87;
then A32: [x1,a] in union FA by A22, A26, TARSKI:def_4;
[x1,a] in [:{x1}, the carrier of T2:] by A30, ZFMISC_1:105;
then [x1,a] in D /\ [:{x1}, the carrier of T2:] by A1, A32, XBOOLE_0:def_4;
then (pr2 ( the carrier of T1, the carrier of T2)) . (x1,a) in (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) by A31, FUNCT_1:def_6;
hence a in X2 by A17, A30, FUNCT_3:def_5; ::_thesis: verum
end;
tx2 in tX2 by A24, A21, A26, ZFMISC_1:87;
hence ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) by A20, A24, A27, A25, A28; ::_thesis: verum
end;
hence ( t in X2 iff ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) ) ; ::_thesis: verum
end;
hence X2 is open by TOPS_1:25; ::_thesis: verum
end;
end;
theorem Th4: :: NAGATA_2:4
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous
proof
let T be non empty TopSpace; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous
set cT = the carrier of T;
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies for x being Point of T holds dist (pmet,x) is continuous )
assume A1: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ; ::_thesis: for x being Point of T holds dist (pmet,x) is continuous
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def_2;
then reconsider pmet9 = pmet as RealMap of [:T,T:] ;
reconsider pmetR = pmet9 as Function of [:T,T:],R^1 by TOPMETR:17;
let x be Point of T; ::_thesis: dist (pmet,x) is continuous
reconsider distx = dist (pmet,x) as Function of T,R^1 by TOPMETR:17;
pmet9 is continuous by A1;
then A2: pmetR is continuous by JORDAN5A:27;
now__::_thesis:_for_t_being_Point_of_T_holds_distx_is_continuous_at_t
let t be Point of T; ::_thesis: distx is_continuous_at t
for R being Subset of R^1 st R is open & distx . t in R holds
ex U being Subset of T st
( U is open & t in U & distx .: U c= R )
proof
reconsider xt = [x,t] as Point of [:T,T:] by BORSUK_1:def_2;
A3: dom (pr2 ( the carrier of T, the carrier of T)) = [: the carrier of T, the carrier of T:] by FUNCT_3:def_5;
A4: ( pmetR is_continuous_at xt & distx . t = pmet . (x,t) ) by A2, Def2, TMAP_1:50;
let R be Subset of R^1; ::_thesis: ( R is open & distx . t in R implies ex U being Subset of T st
( U is open & t in U & distx .: U c= R ) )
assume ( R is open & distx . t in R ) ; ::_thesis: ex U being Subset of T st
( U is open & t in U & distx .: U c= R )
then consider XU being Subset of [:T,T:] such that
A5: XU is open and
A6: xt in XU and
A7: pmetR .: XU c= R by A4, TMAP_1:43;
set U = (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]);
[x,t] in [:{x}, the carrier of T:] by ZFMISC_1:105;
then [x,t] in XU /\ [:{x}, the carrier of T:] by A6, XBOOLE_0:def_4;
then (pr2 ( the carrier of T, the carrier of T)) . (x,t) in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) by A3, FUNCT_1:def_6;
then A8: t in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) by FUNCT_3:def_5;
A9: distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) c= R
proof
let du be set ; :: according to TARSKI:def_3 ::_thesis: ( not du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) or du in R )
assume du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) ; ::_thesis: du in R
then consider u being set such that
A10: u in dom distx and
A11: u in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) and
A12: distx . u = du by FUNCT_1:def_6;
reconsider u = u as Point of T by A10;
consider xu being set such that
A13: xu in dom (pr2 ( the carrier of T, the carrier of T)) and
A14: xu in XU /\ [:{x}, the carrier of T:] and
A15: (pr2 ( the carrier of T, the carrier of T)) . xu = u by A11, FUNCT_1:def_6;
consider x9, u9 being set such that
A16: ( x9 in the carrier of T & u9 in the carrier of T ) and
A17: xu = [x9,u9] by A13, ZFMISC_1:def_2;
reconsider x9 = x9, u9 = u9 as Point of T by A16;
[x9,u9] in [:{x}, the carrier of T:] by A14, A17, XBOOLE_0:def_4;
then ( (pr2 ( the carrier of T, the carrier of T)) . (x9,u9) = u9 & x9 = x ) by FUNCT_3:def_5, ZFMISC_1:105;
then A18: pmet . (x9,u9) = du by A12, A15, A17, Def2;
A19: dom pmetR = the carrier of [:T,T:] by FUNCT_2:def_1;
[x9,u9] in XU by A14, A17, XBOOLE_0:def_4;
then du in pmetR .: XU by A18, A19, FUNCT_1:def_6;
hence du in R by A7; ::_thesis: verum
end;
(pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) is open by A5, Th3;
hence ex U being Subset of T st
( U is open & t in U & distx .: U c= R ) by A8, A9; ::_thesis: verum
end;
hence distx is_continuous_at t by TMAP_1:43; ::_thesis: verum
end;
then distx is continuous by TMAP_1:50;
hence dist (pmet,x) is continuous by JORDAN5A:27; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Function of [:X,X:],REAL;
let A be Subset of X;
func lower_bound (f,A) -> Function of X,REAL means :Def3: :: NAGATA_2:def 3
for x being Element of X holds it . x = lower_bound ((dist (f,x)) .: A);
existence
ex b1 being Function of X,REAL st
for x being Element of X holds b1 . x = lower_bound ((dist (f,x)) .: A)
proof
deffunc H1( Element of X) -> Element of REAL = lower_bound ((dist (f,$1)) .: A);
consider INF being Function of X,REAL such that
A1: for x being Element of X holds INF . x = H1(x) from FUNCT_2:sch_4();
take INF ; ::_thesis: for x being Element of X holds INF . x = lower_bound ((dist (f,x)) .: A)
thus for x being Element of X holds INF . x = lower_bound ((dist (f,x)) .: A) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X holds b1 . x = lower_bound ((dist (f,x)) .: A) ) & ( for x being Element of X holds b2 . x = lower_bound ((dist (f,x)) .: A) ) holds
b1 = b2
proof
let I1, I2 be Function of X,REAL; ::_thesis: ( ( for x being Element of X holds I1 . x = lower_bound ((dist (f,x)) .: A) ) & ( for x being Element of X holds I2 . x = lower_bound ((dist (f,x)) .: A) ) implies I1 = I2 )
assume that
A2: for x being Element of X holds I1 . x = lower_bound ((dist (f,x)) .: A) and
A3: for x being Element of X holds I2 . x = lower_bound ((dist (f,x)) .: A) ; ::_thesis: I1 = I2
now__::_thesis:_for_x_being_Element_of_X_holds_I1_._x_=_I2_._x
let x be Element of X; ::_thesis: I1 . x = I2 . x
I1 . x = lower_bound ((dist (f,x)) .: A) by A2;
hence I1 . x = I2 . x by A3; ::_thesis: verum
end;
hence I1 = I2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines lower_bound NAGATA_2:def_3_:_
for X being non empty set
for f being Function of [:X,X:],REAL
for A being Subset of X
for b4 being Function of X,REAL holds
( b4 = lower_bound (f,A) iff for x being Element of X holds b4 . x = lower_bound ((dist (f,x)) .: A) );
Lm1: for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
proof
let X be non empty set ; ::_thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X implies ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) )
assume A1: f is_a_pseudometric_of X ; ::_thesis: ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
A2: now__::_thesis:_for_A_being_non_empty_Subset_of_X
for_x_being_Element_of_X_holds_
(_not_(dist_(f,x))_.:_A_is_empty_&_(dist_(f,x))_.:_A_is_bounded_below_)
let A be non empty Subset of X; ::_thesis: for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )
let x be Element of X; ::_thesis: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )
A3: 0 is LowerBound of (dist (f,x)) .: A
proof
let rn be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not rn in (dist (f,x)) .: A or 0 <= rn )
assume rn in (dist (f,x)) .: A ; ::_thesis: 0 <= rn
then consider y being set such that
A4: y in dom (dist (f,x)) and
y in A and
A5: rn = (dist (f,x)) . y by FUNCT_1:def_6;
reconsider y = y as Element of X by A4;
f . (x,y) >= 0 by A1, NAGATA_1:29;
hence rn >= 0 by A5, Def2; ::_thesis: verum
end;
dom (dist (f,x)) = X by FUNCT_2:def_1;
hence ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A3, XXREAL_2:def_9; ::_thesis: verum
end;
now__::_thesis:_for_xy_being_set_st_xy_in_dom_f_holds_
f_._xy_>_-_1
let xy be set ; ::_thesis: ( xy in dom f implies f . xy > - 1 )
assume xy in dom f ; ::_thesis: f . xy > - 1
then consider x, y being set such that
A6: ( x in X & y in X ) and
A7: [x,y] = xy by ZFMISC_1:def_2;
reconsider x = x, y = y as Element of X by A6;
( f . (x,y) >= 0 & 0 > - 1 ) by A1, NAGATA_1:29;
hence f . xy > - 1 by A7; ::_thesis: verum
end;
hence ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) by A2, SEQ_2:def_2; ::_thesis: verum
end;
theorem Th5: :: NAGATA_2:5
for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being non empty Subset of X
for x being Element of X holds (lower_bound (f,A)) . x >= 0
proof
let X be non empty set ; ::_thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being non empty Subset of X
for x being Element of X holds (lower_bound (f,A)) . x >= 0
let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X implies for A being non empty Subset of X
for x being Element of X holds (lower_bound (f,A)) . x >= 0 )
assume A1: f is_a_pseudometric_of X ; ::_thesis: for A being non empty Subset of X
for x being Element of X holds (lower_bound (f,A)) . x >= 0
let A be non empty Subset of X; ::_thesis: for x being Element of X holds (lower_bound (f,A)) . x >= 0
let x be Element of X; ::_thesis: (lower_bound (f,A)) . x >= 0
A2: now__::_thesis:_for_rn_being_real_number_st_rn_in_(dist_(f,x))_.:_A_holds_
rn_>=_0
let rn be real number ; ::_thesis: ( rn in (dist (f,x)) .: A implies rn >= 0 )
assume rn in (dist (f,x)) .: A ; ::_thesis: rn >= 0
then consider y being set such that
A3: y in dom (dist (f,x)) and
y in A and
A4: rn = (dist (f,x)) . y by FUNCT_1:def_6;
(dist (f,x)) . y = f . (x,y) by A3, Def2;
hence rn >= 0 by A1, A3, A4, NAGATA_1:29; ::_thesis: verum
end;
X = dom (dist (f,x)) by FUNCT_2:def_1;
then lower_bound ((dist (f,x)) .: A) >= 0 by A2, SEQ_4:43;
hence (lower_bound (f,A)) . x >= 0 by Def3; ::_thesis: verum
end;
theorem Th6: :: NAGATA_2:6
for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being Subset of X
for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0
proof
let X be non empty set ; ::_thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being Subset of X
for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0
let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X implies for A being Subset of X
for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0 )
assume A1: f is_a_pseudometric_of X ; ::_thesis: for A being Subset of X
for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0
let A be Subset of X; ::_thesis: for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0
let x be Element of X; ::_thesis: ( x in A implies (lower_bound (f,A)) . x = 0 )
assume A2: x in A ; ::_thesis: (lower_bound (f,A)) . x = 0
then reconsider A = A as non empty Subset of X ;
A3: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A1, Lm1;
f is Reflexive by A1, NAGATA_1:def_10;
then f . (x,x) = 0 by METRIC_1:def_2;
then ( X = dom (dist (f,x)) & (dist (f,x)) . x = 0 ) by Def2, FUNCT_2:def_1;
then 0 in (dist (f,x)) .: A by A2, FUNCT_1:def_6;
then lower_bound ((dist (f,x)) .: A) <= 0 by A3, SEQ_4:def_2;
then (lower_bound (f,A)) . x <= 0 by Def3;
hence (lower_bound (f,A)) . x = 0 by A1, Th5; ::_thesis: verum
end;
theorem Th7: :: NAGATA_2:7
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
proof
let T be non empty TopSpace; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( pmet is_a_pseudometric_of the carrier of T implies for x, y being Point of T
for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y) )
assume A1: pmet is_a_pseudometric_of the carrier of T ; ::_thesis: for x, y being Point of T
for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
A2: pmet is symmetric by A1, NAGATA_1:def_10;
let x, y be Point of T; ::_thesis: for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
let A be non empty Subset of T; ::_thesis: abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
A3: for x1, y1 being Point of T holds ((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1))
proof
let x1, y1 be Point of T; ::_thesis: ((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1))
A4: ( not (dist (pmet,x1)) .: A is empty & (dist (pmet,x1)) .: A is bounded_below ) by A1, Lm1;
A5: for rn being real number st rn in (dist (pmet,y1)) .: A holds
rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
proof
let rn be real number ; ::_thesis: ( rn in (dist (pmet,y1)) .: A implies rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1)) )
assume rn in (dist (pmet,y1)) .: A ; ::_thesis: rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
then consider z being set such that
A6: z in dom (dist (pmet,y1)) and
A7: z in A and
A8: (dist (pmet,y1)) . z = rn by FUNCT_1:def_6;
reconsider z = z as Point of T by A6;
A9: (dist (pmet,x1)) . z = pmet . (x1,z) by Def2;
pmet is triangle by A1, NAGATA_1:def_10;
then A10: (pmet . (x1,y1)) + (pmet . (y1,z)) >= pmet . (x1,z) by METRIC_1:def_5;
dom (dist (pmet,x1)) = the carrier of T by FUNCT_2:def_1;
then (dist (pmet,x1)) . z in (dist (pmet,x1)) .: A by A7, FUNCT_1:def_6;
then pmet . (x1,z) >= lower_bound ((dist (pmet,x1)) .: A) by A4, A9, SEQ_4:def_2;
then (pmet . (x1,y1)) + (pmet . (y1,z)) >= (lower_bound ((dist (pmet,x1)) .: A)) + 0 by A10, XXREAL_0:2;
then (pmet . (y1,z)) - 0 >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1)) by XREAL_1:21;
hence rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1)) by A8, Def2; ::_thesis: verum
end;
( not (dist (pmet,y1)) .: A is empty & (dist (pmet,y1)) .: A is bounded_below ) by A1, Lm1;
then (lower_bound ((dist (pmet,y1)) .: A)) - 0 >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1)) by A5, SEQ_4:43;
then A11: (lower_bound ((dist (pmet,y1)) .: A)) - (lower_bound ((dist (pmet,x1)) .: A)) >= 0 - (pmet . (x1,y1)) by XREAL_1:17;
lower_bound ((dist (pmet,y1)) .: A) = (lower_bound (pmet,A)) . y1 by Def3;
hence ((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1)) by A11, Def3; ::_thesis: verum
end;
then ((lower_bound (pmet,A)) . y) - ((lower_bound (pmet,A)) . x) >= - (pmet . (x,y)) ;
then - (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) >= - (pmet . (x,y)) ;
then A12: ((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) <= pmet . (x,y) by XREAL_1:24;
((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) >= - (pmet . (y,x)) by A3;
then ((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) >= - (pmet . (x,y)) by A2, METRIC_1:def_4;
hence abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y) by A12, ABSVALUE:5; ::_thesis: verum
end;
theorem Th8: :: NAGATA_2:8
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist (pmet,p) is continuous ) holds
for A being non empty Subset of T holds lower_bound (pmet,A) is continuous
proof
let T be non empty TopSpace; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist (pmet,p) is continuous ) holds
for A being non empty Subset of T holds lower_bound (pmet,A) is continuous
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist (pmet,p) is continuous ) implies for A being non empty Subset of T holds lower_bound (pmet,A) is continuous )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for p being Point of T holds dist (pmet,p) is continuous ; ::_thesis: for A being non empty Subset of T holds lower_bound (pmet,A) is continuous
let A be non empty Subset of T; ::_thesis: lower_bound (pmet,A) is continuous
reconsider infR = lower_bound (pmet,A) as Function of T,R^1 by TOPMETR:17;
now__::_thesis:_for_t_being_Point_of_T_holds_infR_is_continuous_at_t
let t be Point of T; ::_thesis: infR is_continuous_at t
reconsider dR = dist (pmet,t) as Function of T,R^1 by TOPMETR:17;
for R being Subset of R^1 st R is open & infR . t in R holds
ex U being Subset of T st
( U is open & t in U & infR .: U c= R )
proof
reconsider infRt = infR . t, dRt = dR . t as Point of RealSpace by METRIC_1:def_13;
let R be Subset of R^1; ::_thesis: ( R is open & infR . t in R implies ex U being Subset of T st
( U is open & t in U & infR .: U c= R ) )
assume ( R is open & infR . t in R ) ; ::_thesis: ex U being Subset of T st
( U is open & t in U & infR .: U c= R )
then consider r being real number such that
A3: r > 0 and
A4: Ball (infRt,r) c= R by TOPMETR:15, TOPMETR:def_6;
reconsider dB = Ball (dRt,r) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17;
abs ((dR . t) - (dR . t)) = 0 by ABSVALUE:2;
then dist (dRt,dRt) < r by A3, TOPMETR:11;
then A5: dRt in dB by METRIC_1:11;
dist (pmet,t) is continuous by A2;
then dR is continuous by JORDAN5A:27;
then ( dB is open & dR is_continuous_at t ) by TMAP_1:50, TOPMETR:14, TOPMETR:def_6;
then consider B being Subset of T such that
A6: ( B is open & t in B ) and
A7: dR .: B c= dB by A5, TMAP_1:43;
infR .: B c= R
proof
let Ib be set ; :: according to TARSKI:def_3 ::_thesis: ( not Ib in infR .: B or Ib in R )
assume Ib in infR .: B ; ::_thesis: Ib in R
then consider b being set such that
A8: b in dom infR and
A9: b in B and
A10: infR . b = Ib by FUNCT_1:def_6;
reconsider b = b as Point of T by A8;
reconsider infRb = infR . b, dRb = dR . b as Point of RealSpace by METRIC_1:def_13;
pmet . (t,b) >= 0 by A1, NAGATA_1:29;
then A11: dR . b >= 0 by Def2;
dR . t = pmet . (t,t) by Def2;
then dR . t = 0 by A1, NAGATA_1:28;
then A12: dist (dRt,dRb) = abs (0 - (dR . b)) by TOPMETR:11;
dom dR = the carrier of T by FUNCT_2:def_1;
then dR . b in dR .: B by A9, FUNCT_1:def_6;
then dist (dRt,dRb) < r by A7, METRIC_1:11;
then abs (- (0 - (dR . b))) < r by A12, COMPLEX1:52;
then dR . b < r by A11, ABSVALUE:def_1;
then A13: pmet . (t,b) < r by Def2;
( abs (((lower_bound (pmet,A)) . t) - ((lower_bound (pmet,A)) . b)) <= pmet . (t,b) & dist (infRt,infRb) = abs (((lower_bound (pmet,A)) . t) - ((lower_bound (pmet,A)) . b)) ) by A1, Th7, TOPMETR:11;
then dist (infRt,infRb) < r by A13, XXREAL_0:2;
then infRb in Ball (infRt,r) by METRIC_1:11;
hence Ib in R by A4, A10; ::_thesis: verum
end;
hence ex U being Subset of T st
( U is open & t in U & infR .: U c= R ) by A6; ::_thesis: verum
end;
hence infR is_continuous_at t by TMAP_1:43; ::_thesis: verum
end;
then infR is continuous by TMAP_1:50;
hence lower_bound (pmet,A) is continuous by JORDAN5A:27; ::_thesis: verum
end;
theorem Th9: :: NAGATA_2:9
for X being set
for f being Function of [:X,X:],REAL st f is_metric_of X holds
f is_a_pseudometric_of X
proof
let X be set ; ::_thesis: for f being Function of [:X,X:],REAL st f is_metric_of X holds
f is_a_pseudometric_of X
let f be Function of [:X,X:],REAL; ::_thesis: ( f is_metric_of X implies f is_a_pseudometric_of X )
assume f is_metric_of X ; ::_thesis: f is_a_pseudometric_of X
then for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) by PCOMPS_1:def_6;
then ( f is Reflexive & f is symmetric & f is triangle ) by METRIC_1:def_2, METRIC_1:def_4, METRIC_1:def_5;
hence f is_a_pseudometric_of X by NAGATA_1:def_10; ::_thesis: verum
end;
theorem Th10: :: NAGATA_2:10
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) holds
T is metrizable
proof
let T be non empty TopSpace; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) holds
T is metrizable
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) implies T is metrizable )
assume that
A1: pmet is_metric_of the carrier of T and
A2: for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; ::_thesis: T is metrizable
set PM = SpaceMetr ( the carrier of T,pmet);
reconsider PM = SpaceMetr ( the carrier of T,pmet) as non empty MetrSpace by A1, PCOMPS_1:36;
A3: for x, y being Element of PM holds pmet . (x,y) = dist (x,y)
proof
let x, y be Element of PM; ::_thesis: pmet . (x,y) = dist (x,y)
PM = MetrStruct(# the carrier of T,pmet #) by A1, PCOMPS_1:def_7;
hence pmet . (x,y) = dist (x,y) by METRIC_1:def_1; ::_thesis: verum
end;
A4: Family_open_set PM c= the topology of T
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Family_open_set PM or A in the topology of T )
assume A5: A in Family_open_set PM ; ::_thesis: A in the topology of T
then reconsider AT = A as Subset of T by A1, PCOMPS_2:4;
percases ( AT ` is empty or not AT ` is empty ) ;
suppose AT ` is empty ; ::_thesis: A in the topology of T
then AT ` = ([#] T) ` by XBOOLE_1:37;
then AT = the carrier of T by TOPS_1:1;
hence A in the topology of T by PRE_TOPC:def_1; ::_thesis: verum
end;
supposeA6: not AT ` is empty ; ::_thesis: A in the topology of T
for x being set holds
( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) )
proof
let x be set ; ::_thesis: ( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) )
( x in AT implies ex U being Subset of T st
( U is open & U c= AT & x in U ) )
proof
assume A7: x in AT ; ::_thesis: ex U being Subset of T st
( U is open & U c= AT & x in U )
then reconsider xP = x as Element of PM by A1, PCOMPS_2:4;
consider r being Real such that
A8: r > 0 and
A9: Ball (xP,r) c= AT by A5, A7, PCOMPS_1:def_4;
reconsider xT = x as Element of T by A7;
A10: ex y being set st y in AT ` by A6, XBOOLE_0:def_1;
reconsider B = Ball (xP,r) as Subset of T by A1, PCOMPS_2:4;
set Inf = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;
AT ` c= B ` by A9, SUBSET_1:12;
then consider b being set such that
A11: b in B ` by A10;
B ` = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
proof
thus B ` c= { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } :: according to XBOOLE_0:def_10 ::_thesis: { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } c= B `
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B ` or y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } )
assume A12: y in B ` ; ::_thesis: y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
(lower_bound (pmet,(B `))) . y = 0 by A1, A12, Th6, Th9;
hence y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } by A12; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } or y in B ` )
assume y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ; ::_thesis: y in B `
then consider yT being Point of T such that
A13: y = yT and
A14: (lower_bound (pmet,(B `))) . yT = 0 ;
assume not y in B ` ; ::_thesis: contradiction
then A15: yT in B by A13, XBOOLE_0:def_5;
reconsider yP = yT as Point of PM by A1, PCOMPS_2:4;
pmet is_a_pseudometric_of the carrier of T by A1, Th9;
then A16: ( not (dist (pmet,yT)) .: (B `) is empty & (dist (pmet,yT)) .: (B `) is bounded_below ) by A11, Lm1;
Ball (xP,r) in Family_open_set PM by PCOMPS_1:29;
then consider s being Real such that
A17: s > 0 and
A18: Ball (yP,s) c= Ball (xP,r) by A15, PCOMPS_1:def_4;
lower_bound ((dist (pmet,yT)) .: (B `)) = 0 by A14, Def3;
then consider rn being real number such that
A19: rn in (dist (pmet,yT)) .: (B `) and
A20: rn < 0 + s by A17, A16, SEQ_4:def_2;
consider z being set such that
A21: z in dom (dist (pmet,yT)) and
A22: z in B ` and
A23: rn = (dist (pmet,yT)) . z by A19, FUNCT_1:def_6;
reconsider zT = z as Point of T by A21;
reconsider zP = z as Point of PM by A1, A21, PCOMPS_2:4;
pmet . (yT,zT) < s by A20, A23, Def2;
then dist (yP,zP) < s by A3;
then zP in Ball (yP,s) by METRIC_1:11;
then B ` meets B by A18, A22, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; ::_thesis: verum
end;
then B ` = Cl (B `) by A2, A11;
then A24: B is open by TOPS_1:4;
pmet . (xT,xT) = 0 by A1, PCOMPS_1:def_6;
then dist (xP,xP) < r by A3, A8;
then xP in B by METRIC_1:11;
hence ex U being Subset of T st
( U is open & U c= AT & x in U ) by A9, A24; ::_thesis: verum
end;
hence ( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) ) ; ::_thesis: verum
end;
then AT is open by TOPS_1:25;
hence A in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
the topology of T c= Family_open_set PM
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in the topology of T or A in Family_open_set PM )
assume A25: A in the topology of T ; ::_thesis: A in Family_open_set PM
then reconsider AT = A as Subset of T ;
reconsider AP = A as Subset of PM by A1, A25, PCOMPS_2:4;
percases ( AT ` is empty or not AT ` is empty ) ;
suppose AT ` is empty ; ::_thesis: A in Family_open_set PM
then AT ` = ([#] T) ` by XBOOLE_1:37;
then AT = the carrier of T by TOPS_1:1;
then AT = the carrier of PM by A1, PCOMPS_2:4;
hence A in Family_open_set PM by PCOMPS_1:30; ::_thesis: verum
end;
supposeA26: not AT ` is empty ; ::_thesis: A in Family_open_set PM
for xP being Element of PM st xP in AP holds
ex r being Real st
( r > 0 & Ball (xP,r) c= AP )
proof
let xP be Element of PM; ::_thesis: ( xP in AP implies ex r being Real st
( r > 0 & Ball (xP,r) c= AP ) )
assume A27: xP in AP ; ::_thesis: ex r being Real st
( r > 0 & Ball (xP,r) c= AP )
reconsider xT = xP as Element of T by A1, PCOMPS_2:4;
take r = (lower_bound (pmet,(AT `))) . xT; ::_thesis: ( r > 0 & Ball (xP,r) c= AP )
A28: Ball (xP,r) c= AP
proof
pmet is_a_pseudometric_of the carrier of T by A1, Th9;
then A29: ( not (dist (pmet,xT)) .: (AT `) is empty & (dist (pmet,xT)) .: (AT `) is bounded_below ) by A26, Lm1;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (xP,r) or y in AP )
assume that
A30: y in Ball (xP,r) and
A31: not y in AP ; ::_thesis: contradiction
reconsider yP = y as Point of PM by A30;
A32: dist (xP,yP) < r by A30, METRIC_1:11;
reconsider yT = yP as Point of T by A1, PCOMPS_2:4;
A33: dom (dist (pmet,xT)) = the carrier of T by FUNCT_2:def_1;
yT in AT ` by A31, XBOOLE_0:def_5;
then (dist (pmet,xT)) . yT in (dist (pmet,xT)) .: (AT `) by A33, FUNCT_1:def_6;
then A34: lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT by A29, SEQ_4:def_2;
( (dist (pmet,xT)) . yT = pmet . (xT,yT) & lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT ) by Def2, Def3;
hence contradiction by A3, A32, A34; ::_thesis: verum
end;
AT is open by A25, PRE_TOPC:def_2;
then AT ` = Cl (AT `) by PRE_TOPC:22;
then A35: AT ` = { p where p is Point of T : (lower_bound (pmet,(AT `))) . p = 0 } by A2, A26;
(lower_bound (pmet,(AT `))) . xT > 0
proof
assume (lower_bound (pmet,(AT `))) . xT <= 0 ; ::_thesis: contradiction
then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;
then xT in AT ` by A35;
then AT ` meets AT by A27, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; ::_thesis: verum
end;
hence ( r > 0 & Ball (xP,r) c= AP ) by A28; ::_thesis: verum
end;
hence A in Family_open_set PM by PCOMPS_1:def_4; ::_thesis: verum
end;
end;
end;
then the topology of T = Family_open_set PM by A4, XBOOLE_0:def_10;
hence T is metrizable by A1, PCOMPS_1:def_8; ::_thesis: verum
end;
theorem Th11: :: NAGATA_2:11
for T being non empty TopSpace
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) ) & ( for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T
proof
let T be non empty TopSpace; ::_thesis: for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) ) & ( for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T
set cT = the carrier of T;
let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) ) & ( for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable ) implies for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T )
assume that
A1: for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) and
A2: for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable ; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) implies pmet is_a_pseudometric_of the carrier of T )
assume A3: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ; ::_thesis: pmet is_a_pseudometric_of the carrier of T
now__::_thesis:_for_a,_b,_c_being_Point_of_T_holds_
(_pmet_._(a,a)_=_0_&_pmet_._(a,c)_<=_(pmet_._(a,b))_+_(pmet_._(c,b))_)
let a, b, c be Point of T; ::_thesis: ( pmet . (a,a) = 0 & pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) )
thus pmet . (a,a) = 0 ::_thesis: pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b))
proof
set aa = [a,a];
set F = FS2 # [a,a];
now__::_thesis:_for_n_being_Element_of_NAT_holds_(FS2_#_[a,a])_._n_=_0_*_((FS2_#_[a,a])_._n)
let n be Element of NAT ; ::_thesis: (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n)
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A4: FS2 . n = pmet1 and
A5: pmet1 is_a_pseudometric_of the carrier of T by A1;
pmet1 . (a,a) = 0 by A5, NAGATA_1:28;
hence (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n) by A4, SEQFUNC:def_10; ::_thesis: verum
end;
then A6: FS2 # [a,a] = 0 (#) (FS2 # [a,a]) by SEQ_1:9;
FS2 # [a,a] is summable by A2;
then Sum (FS2 # [a,a]) = 0 * (Sum (FS2 # [a,a])) by A6, SERIES_1:10;
hence pmet . (a,a) = 0 by A3; ::_thesis: verum
end;
thus pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) ::_thesis: verum
proof
set ab = [a,b];
set cb = [c,b];
set ac = [a,c];
set Fac = FS2 # [a,c];
set Fab = FS2 # [a,b];
set Fcb = FS2 # [c,b];
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_0_<=_(FS2_#_[a,c])_._n_&_(FS2_#_[a,c])_._n_<=_((FS2_#_[a,b])_+_(FS2_#_[c,b]))_._n_)
let n be Element of NAT ; ::_thesis: ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n )
A8: ( (FS2 . n) . [a,c] = (FS2 # [a,c]) . n & (FS2 . n) . [a,b] = (FS2 # [a,b]) . n ) by SEQFUNC:def_10;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A9: FS2 . n = pmet1 and
A10: pmet1 is_a_pseudometric_of the carrier of T by A1;
A11: 0 <= pmet1 . (a,c) by A10, NAGATA_1:29;
pmet1 . (a,c) <= (pmet1 . (a,b)) + (pmet1 . (c,b)) by A10, NAGATA_1:28;
then (FS2 # [a,c]) . n <= ((FS2 # [a,b]) . n) + ((FS2 # [c,b]) . n) by A9, A8, SEQFUNC:def_10;
hence ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n ) by A9, A11, SEQFUNC:def_10, SEQ_1:7; ::_thesis: verum
end;
A12: ( FS2 # [a,b] is summable & FS2 # [c,b] is summable ) by A2;
then (FS2 # [a,b]) + (FS2 # [c,b]) is summable by SERIES_1:7;
then A13: Sum (FS2 # [a,c]) <= Sum ((FS2 # [a,b]) + (FS2 # [c,b])) by A7, SERIES_1:20;
A14: ( Sum (FS2 # [a,b]) = pmet . [a,b] & Sum (FS2 # [c,b]) = pmet . [c,b] ) by A3;
Sum ((FS2 # [a,b]) + (FS2 # [c,b])) = (Sum (FS2 # [a,b])) + (Sum (FS2 # [c,b])) by A12, SERIES_1:7;
hence pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) by A3, A13, A14; ::_thesis: verum
end;
end;
hence pmet is_a_pseudometric_of the carrier of T by NAGATA_1:28; ::_thesis: verum
end;
theorem Th12: :: NAGATA_2:12
for r being Real
for n being Element of NAT
for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
proof
let r be Real; ::_thesis: for n being Element of NAT
for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
let seq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT st m <= n holds
seq . m <= r ) implies for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) )
assume A1: for m being Element of NAT st m <= n holds
seq . m <= r ; ::_thesis: for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
defpred S1[ Element of NAT ] means ( $1 <= n implies (Partial_Sums seq) . $1 <= r * ($1 + 1) );
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
A4: (Partial_Sums seq) . (m + 1) = ((Partial_Sums seq) . m) + (seq . (m + 1)) by SERIES_1:def_1;
assume A5: m + 1 <= n ; ::_thesis: (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1)
then seq . (m + 1) <= r by A1;
then (Partial_Sums seq) . (m + 1) <= (r * (m + 1)) + r by A3, A5, A4, NAT_1:13, XREAL_1:7;
hence (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1) ; ::_thesis: verum
end;
(Partial_Sums seq) . 0 = seq . 0 by SERIES_1:def_1;
then A6: S1[ 0 ] by A1;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A2);
hence for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) ; ::_thesis: verum
end;
theorem Th13: :: NAGATA_2:13
for seq being Real_Sequence
for k being Element of NAT holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k
proof
let seq be Real_Sequence; ::_thesis: for k being Element of NAT holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k
set PS = Partial_Sums seq;
set absPS = Partial_Sums (abs seq);
defpred S1[ Element of NAT ] means abs ((Partial_Sums seq) . $1) <= (Partial_Sums (abs seq)) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then A2: (abs ((Partial_Sums seq) . k)) + (abs (seq . (k + 1))) <= ((Partial_Sums (abs seq)) . k) + (abs (seq . (k + 1))) by XREAL_1:7;
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SERIES_1:def_1;
then A3: abs ((Partial_Sums seq) . (k + 1)) <= (abs ((Partial_Sums seq) . k)) + (abs (seq . (k + 1))) by COMPLEX1:56;
(abs seq) . (k + 1) = abs (seq . (k + 1)) by SEQ_1:12;
then abs ((Partial_Sums seq) . (k + 1)) <= ((Partial_Sums (abs seq)) . k) + ((abs seq) . (k + 1)) by A3, A2, XXREAL_0:2;
hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum
end;
( (Partial_Sums (abs seq)) . 0 = (abs seq) . 0 & (abs seq) . 0 = abs (seq . 0) ) by SEQ_1:12, SERIES_1:def_1;
then A4: S1[ 0 ] by SERIES_1:def_1;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1);
hence for k being Element of NAT holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k ; ::_thesis: verum
end;
theorem Th14: :: NAGATA_2:14
for T being non empty TopSpace
for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
proof
let T be non empty TopSpace; ::_thesis: for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let FS1 be Functional_Sequence of the carrier of T,REAL; ::_thesis: ( ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) implies for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous )
assume that
A1: for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) and
A2: ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) ; ::_thesis: for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let f be RealMap of T; ::_thesis: ( ( for p being Point of T holds f . p = Sum (FS1 # p) ) implies f is continuous )
assume A3: for p being Point of T holds f . p = Sum (FS1 # p) ; ::_thesis: f is continuous
reconsider fR = f as Function of T,R^1 by TOPMETR:17;
now__::_thesis:_for_p_being_Point_of_T_holds_fR_is_continuous_at_p
let p be Point of T; ::_thesis: fR is_continuous_at p
for R being Subset of R^1 st R is open & fR . p in R holds
ex U being Subset of T st
( U is open & p in U & fR .: U c= R )
proof
reconsider fRp = fR . p as Point of RealSpace by METRIC_1:def_13;
let R be Subset of R^1; ::_thesis: ( R is open & fR . p in R implies ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) )
assume ( R is open & fR . p in R ) ; ::_thesis: ex U being Subset of T st
( U is open & p in U & fR .: U c= R )
then consider rn being real number such that
A4: rn > 0 and
A5: Ball (fRp,rn) c= R by TOPMETR:15, TOPMETR:def_6;
set r2 = rn / 2;
set r4 = rn / 4;
reconsider r2 = rn / 2, r4 = rn / 4 as Real ;
A6: r4 > 0 by A4, XREAL_1:224;
consider seq being Real_Sequence such that
A7: seq is summable and
A8: for n being Element of NAT
for q being Point of T holds (FS1 # q) . n <= seq . n by A2;
Partial_Sums seq is convergent by A7, SERIES_1:def_2;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs (((Partial_Sums seq) . m) - (lim (Partial_Sums seq))) < r4 by A6, SEQ_2:def_7;
defpred S1[ set , set ] means ex SS being Subset of T st
( SS = $2 & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . $1 = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) );
A10: for k being set st k in {0} \/ (Seg n) holds
ex U being set st
( U in bool the carrier of T & S1[k,U] )
proof
let k be set ; ::_thesis: ( k in {0} \/ (Seg n) implies ex U being set st
( U in bool the carrier of T & S1[k,U] ) )
assume k in {0} \/ (Seg n) ; ::_thesis: ex U being set st
( U in bool the carrier of T & S1[k,U] )
then ( k in Seg n or k in {0} ) by XBOOLE_0:def_3;
then reconsider k = k as Element of NAT by TARSKI:def_1;
consider f1 being RealMap of T such that
A11: FS1 . k = f1 and
A12: f1 is continuous and
for p being Point of T holds f1 . p >= 0 by A1;
reconsider f19 = f1 as Function of T,R^1 by TOPMETR:17;
reconsider f1p = f19 . p as Point of RealSpace by METRIC_1:def_13;
set B = Ball (f1p,(r2 / (n + 1)));
reconsider B = Ball (f1p,(r2 / (n + 1))) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17;
( dist (f1p,f1p) = 0 & r2 > 0 ) by A4, METRIC_1:1, XREAL_1:215;
then dist (f1p,f1p) < r2 / (n + 1) by XREAL_1:139;
then A13: f1p in B by METRIC_1:11;
f19 is continuous by A12, JORDAN5A:27;
then ( B is open & f19 is_continuous_at p ) by TMAP_1:50, TOPMETR:14, TOPMETR:def_6;
then consider U being Subset of T such that
A14: ( U is open & p in U ) and
A15: f19 .: U c= B by A13, TMAP_1:43;
for f1 being RealMap of T st FS1 . k = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: U c= Ball (f1p,(r2 / (n + 1))) by A11, A15;
hence ex U being set st
( U in bool the carrier of T & S1[k,U] ) by A14; ::_thesis: verum
end;
consider FSn being Function of ({0} \/ (Seg n)),(bool the carrier of T) such that
A16: for k being set st k in {0} \/ (Seg n) holds
S1[k,FSn . k] from FUNCT_2:sch_1(A10);
A17: for k being Element of NAT
for q being Point of T holds (FS1 # q) . k >= 0
proof
let k be Element of NAT ; ::_thesis: for q being Point of T holds (FS1 # q) . k >= 0
let q be Point of T; ::_thesis: (FS1 # q) . k >= 0
( ex f1 being RealMap of T st
( FS1 . k = f1 & f1 is continuous & ( for q being Point of T holds f1 . q >= 0 ) ) & (FS1 . k) . q = (FS1 # q) . k ) by A1, SEQFUNC:def_10;
hence (FS1 # q) . k >= 0 ; ::_thesis: verum
end;
A18: for k being Element of NAT holds (seq ^\ (n + 1)) . k >= 0
proof
let k be Element of NAT ; ::_thesis: (seq ^\ (n + 1)) . k >= 0
( 0 <= (FS1 # p) . ((n + 1) + k) & seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k ) by A17, NAT_1:def_3;
hence (seq ^\ (n + 1)) . k >= 0 by A8; ::_thesis: verum
end;
reconsider RNG = rng FSn as Subset-Family of T ;
A19: RNG is open
proof
let Q be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not Q in RNG or Q is open )
assume Q in RNG ; ::_thesis: Q is open
then consider x being set such that
A20: x in dom FSn and
A21: FSn . x = Q by FUNCT_1:def_3;
ex SS being Subset of T st
( SS = FSn . x & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . x = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by A16, A20;
hence Q is open by A21; ::_thesis: verum
end;
0 in {0} by TARSKI:def_1;
then 0 in {0} \/ (Seg n) by XBOOLE_0:def_3;
then reconsider RNG = RNG as non empty Subset-Family of T by FUNCT_2:4;
A22: ( lim (Partial_Sums seq) = Sum seq & Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) ) by A7, SERIES_1:15, SERIES_1:def_3;
abs (((Partial_Sums seq) . n) - (lim (Partial_Sums seq))) < r4 by A9;
then abs (- (Sum (seq ^\ (n + 1)))) < r4 by A22;
then A23: abs (Sum (seq ^\ (n + 1))) < r4 by COMPLEX1:52;
seq ^\ (n + 1) is summable by A7, SERIES_1:12;
then Sum (seq ^\ (n + 1)) >= 0 by A18, SERIES_1:18;
then A24: Sum (seq ^\ (n + 1)) < r4 by A23, ABSVALUE:def_1;
A25: for q being Point of T holds
( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
proof
let q be Point of T; ::_thesis: ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
set F = FS1 # q;
A26: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_0_<=_((FS1_#_q)_^\_(n_+_1))_._k_&_((FS1_#_q)_^\_(n_+_1))_._k_<=_(seq_^\_(n_+_1))_._k_)
let k be Element of NAT ; ::_thesis: ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k )
A27: seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k by NAT_1:def_3;
( 0 <= (FS1 # q) . ((n + 1) + k) & (FS1 # q) . ((n + 1) + k) <= seq . ((n + 1) + k) ) by A8, A17;
hence ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) by A27, NAT_1:def_3; ::_thesis: verum
end;
A28: for k being Element of NAT holds
( 0 <= (FS1 # q) . k & (FS1 # q) . k <= seq . k ) by A8, A17;
then FS1 # q is summable by A7, SERIES_1:20;
then A29: (FS1 # q) ^\ (n + 1) is summable by SERIES_1:12;
seq ^\ (n + 1) is summable by A7, SERIES_1:12;
then Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1)) by A26, SERIES_1:20;
hence ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A7, A24, A28, A26, A29, SERIES_1:18, SERIES_1:20, XXREAL_0:2; ::_thesis: verum
end;
A30: fR .: (meet RNG) c= R
proof
let fRq be set ; :: according to TARSKI:def_3 ::_thesis: ( not fRq in fR .: (meet RNG) or fRq in R )
assume fRq in fR .: (meet RNG) ; ::_thesis: fRq in R
then consider q being set such that
A31: q in dom fR and
A32: q in meet RNG and
A33: fRq = fR . q by FUNCT_1:def_6;
reconsider q = q as Point of T by A31;
set sp = FS1 # p;
set sq = FS1 # q;
set spn = (FS1 # p) ^\ (n + 1);
set sqn = (FS1 # q) ^\ (n + 1);
set absPSpq = Partial_Sums (abs ((FS1 # p) - (FS1 # q)));
for k being Element of NAT st k <= n holds
(abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)
proof
let k be Element of NAT ; ::_thesis: ( k <= n implies (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1) )
assume A34: k <= n ; ::_thesis: (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)
( k = 0 or k >= 1 ) by NAT_1:14;
then ( k in {0} or k in Seg n ) by A34, FINSEQ_1:1, TARSKI:def_1;
then A35: k in {0} \/ (Seg n) by XBOOLE_0:def_3;
then FSn . k in RNG by FUNCT_2:4;
then A36: q in FSn . k by A32, SETFAM_1:def_1;
dom ((FS1 # p) - (FS1 # q)) = NAT by FUNCT_2:def_1;
then A37: ((FS1 # p) - (FS1 # q)) . k = ((FS1 # p) . k) - ((FS1 # q) . k) by VALUED_1:13;
consider f1 being RealMap of T such that
A38: FS1 . k = f1 and
f1 is continuous and
for p being Point of T holds f1 . p >= 0 by A1;
reconsider f1p = f1 . p, f1q = f1 . q as Point of RealSpace by METRIC_1:def_13;
ex SS being Subset of T st
( SS = FSn . k & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . k = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by A16, A35;
then A39: f1 .: (FSn . k) c= Ball (f1p,(r2 / (n + 1))) by A38;
dom f1 = the carrier of T by FUNCT_2:def_1;
then f1q in f1 .: (FSn . k) by A36, FUNCT_1:def_6;
then dist (f1p,f1q) < r2 / (n + 1) by A39, METRIC_1:11;
then A40: abs ((f1 . p) - (f1 . q)) < r2 / (n + 1) by TOPMETR:11;
f1 . p = (FS1 # p) . k by A38, SEQFUNC:def_10;
then abs (((FS1 # p) . k) - ((FS1 # q) . k)) < r2 / (n + 1) by A38, A40, SEQFUNC:def_10;
hence (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1) by A37, SEQ_1:12; ::_thesis: verum
end;
then A41: (Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n <= (r2 / (n + 1)) * (n + 1) by Th12;
set PSp = Partial_Sums (FS1 # p);
set PSq = Partial_Sums (FS1 # q);
set PSpq = Partial_Sums ((FS1 # p) - (FS1 # q));
( (Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q)) = Partial_Sums ((FS1 # p) - (FS1 # q)) & dom ((Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q))) = NAT ) by SEQ_1:1, SERIES_1:6;
then A42: abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) = abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n) by VALUED_1:13;
abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n) <= (Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n by Th13;
then abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= (r2 / (n + 1)) * (n + 1) by A42, A41, XXREAL_0:2;
then A43: abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= r2 by XCMPLX_1:87;
0 <= Sum ((FS1 # p) ^\ (n + 1)) by A25;
then A44: abs (Sum ((FS1 # p) ^\ (n + 1))) = Sum ((FS1 # p) ^\ (n + 1)) by ABSVALUE:def_1;
0 <= Sum ((FS1 # q) ^\ (n + 1)) by A25;
then A45: abs (Sum ((FS1 # q) ^\ (n + 1))) = Sum ((FS1 # q) ^\ (n + 1)) by ABSVALUE:def_1;
reconsider fRq = fR . q as Point of RealSpace by METRIC_1:def_13;
A46: abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) <= (abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1)))) by COMPLEX1:57;
A47: ( fRp = Sum (FS1 # p) & fRq = Sum (FS1 # q) ) by A3;
( Sum (FS1 # p) = ((Partial_Sums (FS1 # p)) . n) + (Sum ((FS1 # p) ^\ (n + 1))) & Sum (FS1 # q) = ((Partial_Sums (FS1 # q)) . n) + (Sum ((FS1 # q) ^\ (n + 1))) ) by A25, SERIES_1:15;
then abs ((fR . p) - (fR . q)) = abs ((((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) + ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) by A47;
then A48: abs ((fR . p) - (fR . q)) <= (abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) by COMPLEX1:56;
( Sum ((FS1 # p) ^\ (n + 1)) < r4 & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A25;
then (abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1)))) < r4 + r4 by A44, A45, XREAL_1:8;
then abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) < r2 by A46, XXREAL_0:2;
then (abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) < r2 + r2 by A43, XREAL_1:8;
then abs ((fR . p) - (fR . q)) < rn by A48, XXREAL_0:2;
then dist (fRp,fRq) < rn by TOPMETR:11;
then fRq in Ball (fRp,rn) by METRIC_1:11;
hence fRq in R by A5, A33; ::_thesis: verum
end;
now__::_thesis:_for_Fx_being_set_st_Fx_in_RNG_holds_
p_in_Fx
let Fx be set ; ::_thesis: ( Fx in RNG implies p in Fx )
assume Fx in RNG ; ::_thesis: p in Fx
then consider x being set such that
A49: x in dom FSn and
A50: FSn . x = Fx by FUNCT_1:def_3;
ex SS being Subset of T st
( SS = FSn . x & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . x = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by A16, A49;
hence p in Fx by A50; ::_thesis: verum
end;
then p in meet RNG by SETFAM_1:def_1;
hence ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) by A19, A30, TOPS_2:20; ::_thesis: verum
end;
hence fR is_continuous_at p by TMAP_1:43; ::_thesis: verum
end;
then fR is continuous by TMAP_1:50;
hence f is continuous by JORDAN5A:27; ::_thesis: verum
end;
theorem Th15: :: NAGATA_2:15
for T being non empty TopSpace
for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
proof
let T be non empty TopSpace; ::_thesis: for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
set Geo = (1 / 2) GeoSeq ;
set cT = the carrier of T;
set cTT = the carrier of [:T,T:];
let s be Real; ::_thesis: for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) implies for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) )
assume A1: for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
set SGeo = s (#) ((1 / 2) GeoSeq);
deffunc H1( Nat) -> Element of bool [:[: the carrier of T, the carrier of T:],REAL:] = (((1 / 2) GeoSeq) . $1) (#) (FS2 . $1);
consider GeoF being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL such that
A2: for n being Nat holds GeoF . n = H1(n) from SEQFUNC:sch_1();
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then reconsider GeoF9 = GeoF as Functional_Sequence of the carrier of [:T,T:],REAL ;
A3: for pq being Element of [: the carrier of T, the carrier of T:]
for k being Element of NAT holds
( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: for k being Element of NAT holds
( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )
let k be Element of NAT ; ::_thesis: ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )
consider x, y being set such that
A4: ( x in the carrier of T & y in the carrier of T ) and
A5: [x,y] = pq by ZFMISC_1:def_2;
reconsider x = x, y = y as Point of T by A4;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A6: FS2 . k = pmet1 and
A7: pmet1 is_a_pseudometric_of the carrier of T and
A8: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A1;
A9: 0 <= pmet1 . (x,y) by A7, NAGATA_1:29;
dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by A6, FUNCT_2:def_1;
then A10: (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def_5
.= (GeoF . k) . pq by A2
.= (GeoF # pq) . k by SEQFUNC:def_10 ;
(1 / 2) |^ k > 0 by NEWTON:83;
then A11: ((1 / 2) GeoSeq) . k > 0 by PREPOWER:def_1;
then (((1 / 2) GeoSeq) . k) * (pmet1 . pq) <= (((1 / 2) GeoSeq) . k) * s by A8, XREAL_1:64;
hence ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k ) by A6, A5, A10, A9, A11, SEQ_1:9; ::_thesis: verum
end;
A12: for n being Element of NAT ex f being RealMap of [:T,T:] st
( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )
proof
let n be Element of NAT ; ::_thesis: ex f being RealMap of [:T,T:] st
( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A13: FS2 . n = pmet1 and
pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
A14: for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A1;
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then reconsider pmet19 = pmet1 as RealMap of [:T,T:] ;
reconsider pR = pmet19 as Function of [:T,T:],R^1 by TOPMETR:17;
pmet19 is continuous by A14;
then pR is continuous by JORDAN5A:27;
then consider fR being Function of [:T,T:],R^1 such that
A15: for pq9 being Point of [:T,T:]
for rn being real number st pR . pq9 = rn holds
fR . pq9 = (((1 / 2) GeoSeq) . n) * rn and
A16: fR is continuous by JGRAPH_2:23;
reconsider f = fR as RealMap of [:T,T:] by TOPMETR:17;
A17: dom f = the carrier of [:T,T:] by FUNCT_2:def_1;
take f ; ::_thesis: ( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )
A18: dom pmet1 = [: the carrier of T, the carrier of T:] by FUNCT_2:def_1;
A19: GeoF9 . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;
then A20: dom (FS2 . n) = dom (GeoF9 . n) by VALUED_1:def_5;
A21: [: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def_2;
A22: now__::_thesis:_for_pq9_being_Point_of_[:T,T:]_st_pq9_in_dom_(GeoF9_._n)_holds_
(GeoF9_._n)_._pq9_=_f_._pq9
let pq9 be Point of [:T,T:]; ::_thesis: ( pq9 in dom (GeoF9 . n) implies (GeoF9 . n) . pq9 = f . pq9 )
assume pq9 in dom (GeoF9 . n) ; ::_thesis: (GeoF9 . n) . pq9 = f . pq9
(GeoF9 . n) . pq9 = (((1 / 2) GeoSeq) . n) * (pmet1 . pq9) by A13, A19, A20, A18, A21, VALUED_1:def_5;
hence (GeoF9 . n) . pq9 = f . pq9 by A15; ::_thesis: verum
end;
now__::_thesis:_for_pq9_being_Point_of_[:T,T:]_holds_f_._pq9_>=_0
let pq9 be Point of [:T,T:]; ::_thesis: f . pq9 >= 0
reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
( (GeoF9 . n) . pq9 = (GeoF # pq) . n & (GeoF # pq) . n >= 0 ) by A3, SEQFUNC:def_10;
hence f . pq9 >= 0 by A13, A20, A18, A22; ::_thesis: verum
end;
hence ( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) ) by A13, A16, A20, A18, A17, A21, A22, JORDAN5A:27, PARTFUN1:5; ::_thesis: verum
end;
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) implies ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) )
assume A23: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ; ::_thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
A24: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (GeoF # pq)
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: pmet . pq = Sum (GeoF # pq)
now__::_thesis:_for_z_being_set_st_z_in_NAT_holds_
(((1_/_2)_GeoSeq)_(#)_(FS2_#_pq))_._z_=_(GeoF_#_pq)_._z
let z be set ; ::_thesis: ( z in NAT implies (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z )
assume z in NAT ; ::_thesis: (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z
then reconsider k = z as Element of NAT ;
ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . k = pmet1 & pmet1 is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s ) & ( for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous ) ) by A1;
then dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by FUNCT_2:def_1;
then (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def_5
.= (GeoF . k) . pq by A2
.= (GeoF # pq) . k by SEQFUNC:def_10 ;
then (GeoF # pq) . k = (((1 / 2) GeoSeq) . k) * ((FS2 # pq) . k) by SEQFUNC:def_10
.= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . k by SEQ_1:8 ;
hence (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z ; ::_thesis: verum
end;
then ((1 / 2) GeoSeq) (#) (FS2 # pq) = GeoF # pq by FUNCT_2:12;
hence pmet . pq = Sum (GeoF # pq) by A23; ::_thesis: verum
end;
A25: for n being Element of NAT ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st
( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )
proof
let n be Element of NAT ; ::_thesis: ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st
( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A26: FS2 . n = pmet1 and
A27: pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A1;
deffunc H2( Element of the carrier of T, Element of the carrier of T) -> Element of REAL = (((1 / 2) GeoSeq) . n) * (pmet1 . ($1,$2));
consider GF being Function of [: the carrier of T, the carrier of T:],REAL such that
A28: for p, q being Point of T holds GF . (p,q) = H2(p,q) from BINOP_1:sch_4();
now__::_thesis:_for_a,_b,_c_being_Point_of_T_holds_
(_GF_._(a,a)_=_0_&_GF_._(a,c)_<=_(GF_._(a,b))_+_(GF_._(c,b))_)
let a, b, c be Point of T; ::_thesis: ( GF . (a,a) = 0 & GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) )
(1 / 2) |^ n > 0 by NEWTON:83;
then A29: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def_1;
pmet1 . (a,c) <= (pmet1 . (a,b)) + (pmet1 . (c,b)) by A27, NAGATA_1:28;
then (pmet1 . (a,c)) * (((1 / 2) GeoSeq) . n) <= ((pmet1 . (a,b)) + (pmet1 . (c,b))) * (((1 / 2) GeoSeq) . n) by A29, XREAL_1:64;
then A30: GF . (a,c) <= ((((1 / 2) GeoSeq) . n) * (pmet1 . (a,b))) + ((((1 / 2) GeoSeq) . n) * (pmet1 . (c,b))) by A28;
( GF . (a,a) = (((1 / 2) GeoSeq) . n) * (pmet1 . (a,a)) & pmet1 . (a,a) = 0 ) by A27, A28, NAGATA_1:28;
hence GF . (a,a) = 0 ; ::_thesis: GF . (a,c) <= (GF . (a,b)) + (GF . (c,b))
(((1 / 2) GeoSeq) . n) * (pmet1 . (a,b)) = GF . (a,b) by A28;
hence GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) by A28, A30; ::_thesis: verum
end;
then A31: GF is_a_pseudometric_of the carrier of T by NAGATA_1:28;
A32: GeoF . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;
then A33: dom (FS2 . n) = dom (GeoF . n) by VALUED_1:def_5;
A34: now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_dom_(GeoF_._n)_holds_
(GeoF_._n)_._(x,y)_=_GF_._(x,y)
let x, y be set ; ::_thesis: ( [x,y] in dom (GeoF . n) implies (GeoF . n) . (x,y) = GF . (x,y) )
assume A35: [x,y] in dom (GeoF . n) ; ::_thesis: (GeoF . n) . (x,y) = GF . (x,y)
then reconsider x9 = x, y9 = y as Point of T by ZFMISC_1:87;
GF . (x9,y9) = (((1 / 2) GeoSeq) . n) * (pmet1 . (x9,y9)) by A28;
hence (GeoF . n) . (x,y) = GF . (x,y) by A26, A32, A35, VALUED_1:def_5; ::_thesis: verum
end;
( dom pmet1 = [: the carrier of T, the carrier of T:] & dom GF = [: the carrier of T, the carrier of T:] ) by FUNCT_2:def_1;
hence ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st
( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T ) by A26, A33, A34, A31, BINOP_1:20; ::_thesis: verum
end;
1 / 2 < 1 ;
then abs (1 / 2) < 1 by ABSVALUE:def_1;
then A36: (1 / 2) GeoSeq is summable by SERIES_1:24;
A37: for pq being Element of [: the carrier of T, the carrier of T:]
for pq9 being Point of [:T,T:] st pq = pq9 holds
GeoF # pq = GeoF9 # pq9
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: for pq9 being Point of [:T,T:] st pq = pq9 holds
GeoF # pq = GeoF9 # pq9
let pq9 be Point of [:T,T:]; ::_thesis: ( pq = pq9 implies GeoF # pq = GeoF9 # pq9 )
assume A38: pq = pq9 ; ::_thesis: GeoF # pq = GeoF9 # pq9
now__::_thesis:_for_x_being_Element_of_NAT_holds_(GeoF_#_pq)_._x_=_(GeoF9_#_pq9)_._x
let x be Element of NAT ; ::_thesis: (GeoF # pq) . x = (GeoF9 # pq9) . x
(GeoF # pq) . x = (GeoF . x) . pq by SEQFUNC:def_10;
hence (GeoF # pq) . x = (GeoF9 # pq9) . x by A38, SEQFUNC:def_10; ::_thesis: verum
end;
hence GeoF # pq = GeoF9 # pq9 by FUNCT_2:63; ::_thesis: verum
end;
A39: ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= seq . n ) )
proof
take s (#) ((1 / 2) GeoSeq) ; ::_thesis: ( s (#) ((1 / 2) GeoSeq) is summable & ( for n being Element of NAT
for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) )
thus s (#) ((1 / 2) GeoSeq) is summable by A36, SERIES_1:10; ::_thesis: for n being Element of NAT
for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n
now__::_thesis:_for_n_being_Element_of_NAT_
for_pq9_being_Point_of_[:T,T:]_holds_(GeoF9_#_pq9)_._n_<=_(s_(#)_((1_/_2)_GeoSeq))_._n
let n be Element of NAT ; ::_thesis: for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n
let pq9 be Point of [:T,T:]; ::_thesis: (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n
reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
(GeoF9 # pq9) . n = (GeoF # pq) . n by A37;
hence (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n by A3; ::_thesis: verum
end;
hence for n being Element of NAT
for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ; ::_thesis: verum
end;
A40: now__::_thesis:_for_pmet19_being_RealMap_of_[:T,T:]_st_pmet_=_pmet19_holds_
pmet19_is_continuous
let pmet19 be RealMap of [:T,T:]; ::_thesis: ( pmet = pmet19 implies pmet19 is continuous )
assume A41: pmet = pmet19 ; ::_thesis: pmet19 is continuous
for pq9 being Point of [:T,T:] holds pmet19 . pq9 = Sum (GeoF9 # pq9)
proof
let pq9 be Point of [:T,T:]; ::_thesis: pmet19 . pq9 = Sum (GeoF9 # pq9)
reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
pmet . pq = Sum (GeoF # pq) by A24;
hence pmet19 . pq9 = Sum (GeoF9 # pq9) by A37, A41; ::_thesis: verum
end;
hence pmet19 is continuous by A12, A39, Th14; ::_thesis: verum
end;
for pq being Element of [: the carrier of T, the carrier of T:] holds GeoF # pq is summable
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: GeoF # pq is summable
for k being Element of NAT holds
( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k & s (#) ((1 / 2) GeoSeq) is summable ) by A3, A36, SERIES_1:10;
hence GeoF # pq is summable by SERIES_1:20; ::_thesis: verum
end;
hence ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) by A25, A24, A40, Th11; ::_thesis: verum
end;
theorem Th16: :: NAGATA_2:16
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
proof
let T be non empty TopSpace; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
set rn = 0 ;
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0 )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ; ::_thesis: for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
let A be non empty Subset of T; ::_thesis: for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
let p be Point of T; ::_thesis: ( p in Cl A implies (lower_bound (pmet,A)) . p = 0 )
A3: dom (lower_bound (pmet,A)) = the carrier of T by FUNCT_2:def_1;
reconsider Z = {0}, infA = (lower_bound (pmet,A)) .: A as Subset of R^1 by TOPMETR:17;
infA c= Z
proof
let infa be set ; :: according to TARSKI:def_3 ::_thesis: ( not infa in infA or infa in Z )
assume infa in infA ; ::_thesis: infa in Z
then ex a being set st
( a in dom (lower_bound (pmet,A)) & a in A & infa = (lower_bound (pmet,A)) . a ) by FUNCT_1:def_6;
then infa = 0 by A1, Th6;
hence infa in Z by TARSKI:def_1; ::_thesis: verum
end;
then A4: Cl infA c= Cl Z by PRE_TOPC:19;
reconsider InfA = lower_bound (pmet,A) as Function of T,R^1 by TOPMETR:17;
for p being Point of T holds dist (pmet,p) is continuous by A2, Th4;
then lower_bound (pmet,A) is continuous by A1, Th8;
then InfA is continuous by JORDAN5A:27;
then A5: InfA .: (Cl A) c= Cl (InfA .: A) by TOPS_2:45;
assume p in Cl A ; ::_thesis: (lower_bound (pmet,A)) . p = 0
then A6: (lower_bound (pmet,A)) . p in (lower_bound (pmet,A)) .: (Cl A) by A3, FUNCT_1:def_6;
Z is closed by PCOMPS_1:7, TOPMETR:17;
then Z = Cl Z by PRE_TOPC:22;
then InfA .: (Cl A) c= Z by A4, A5, XBOOLE_1:1;
hence (lower_bound (pmet,A)) . p = 0 by A6, TARSKI:def_1; ::_thesis: verum
end;
theorem Th17: :: NAGATA_2:17
for T being non empty TopSpace st T is T_1 holds
for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) holds
( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable )
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1 implies for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) holds
( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable ) )
assume A1: T is T_1 ; ::_thesis: for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) holds
( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable )
set cT = the carrier of T;
set Geo = (1 / 2) GeoSeq ;
let s be Real; ::_thesis: for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) holds
( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable )
let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) implies ( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable ) )
assume that
A2: for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) and
A3: for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ; ::_thesis: ( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable )
deffunc H1( Element of the carrier of T, Element of the carrier of T) -> Element of REAL = Sum (((1 / 2) GeoSeq) (#) (FS2 # [$1,$2]));
consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A4: for p, q being Point of T holds pmet . (p,q) = H1(p,q) from BINOP_1:sch_4();
A5: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq))
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq))
consider p, q being set such that
A6: ( p in the carrier of T & q in the carrier of T ) and
A7: pq = [p,q] by ZFMISC_1:def_2;
pmet . pq = pmet . (p,q) by A7;
hence pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) by A4, A6, A7; ::_thesis: verum
end;
A8: for pq being Element of [: the carrier of T, the carrier of T:]
for n being Element of NAT holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: for n being Element of NAT holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )
let n be Element of NAT ; ::_thesis: ( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )
consider x, y being set such that
A9: ( x in the carrier of T & y in the carrier of T ) and
A10: [x,y] = pq by ZFMISC_1:def_2;
reconsider x = x, y = y as Point of T by A9;
A11: (((1 / 2) GeoSeq) . n) * s = (s (#) ((1 / 2) GeoSeq)) . n by SEQ_1:9;
(1 / 2) |^ n > 0 by NEWTON:83;
then A12: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def_1;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A13: FS2 . n = pmet1 and
A14: pmet1 is_a_pseudometric_of the carrier of T and
A15: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
A16: 0 <= pmet1 . (x,y) by A14, NAGATA_1:29;
A17: pmet1 . pq = (FS2 # pq) . n by A13, SEQFUNC:def_10;
then (((1 / 2) GeoSeq) . n) * ((FS2 # pq) . n) <= (((1 / 2) GeoSeq) . n) * s by A15, A12, XREAL_1:64;
hence ( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) by A10, A16, A12, A17, A11, SEQ_1:8; ::_thesis: verum
end;
A18: for p, q being Point of T st pmet . (p,q) = 0 holds
p = q
proof
let p, q be Point of T; ::_thesis: ( pmet . (p,q) = 0 implies p = q )
assume that
A19: pmet . (p,q) = 0 and
A20: p <> q ; ::_thesis: contradiction
set Q = {q};
A21: not p in {q} by A20, TARSKI:def_1;
set pq = [p,q];
A22: Sum (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) = 0 by A5, A19;
A23: for n being Element of NAT holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n & (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) by A8;
{q} is closed by A1, URYSOHN1:19;
then consider n being Element of NAT such that
A24: for pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet1 holds
(lower_bound (pmet1,{q})) . p > 0 by A3, A21;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A25: FS2 . n = pmet1 and
A26: pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
(lower_bound (pmet1,{q})) . p > 0 by A24, A25;
then A27: lower_bound ((dist (pmet1,p)) .: {q}) > 0 by Def3;
1 / 2 < 1 ;
then abs (1 / 2) < 1 by ABSVALUE:def_1;
then (1 / 2) GeoSeq is summable by SERIES_1:24;
then s (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then ((1 / 2) GeoSeq) (#) (FS2 # [p,q]) is summable by A23, SERIES_1:20;
then (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n = 0 by A23, A22, RSSPACE:17;
then A28: (((1 / 2) GeoSeq) . n) * ((FS2 # [p,q]) . n) = 0 by SEQ_1:8;
(1 / 2) |^ n > 0 by NEWTON:83;
then ((1 / 2) GeoSeq) . n <> 0 by PREPOWER:def_1;
then A29: (FS2 # [p,q]) . n = 0 by A28, XCMPLX_1:6;
A30: pmet1 . (p,q) = (dist (pmet1,p)) . q by Def2;
( dom (dist (pmet1,p)) = the carrier of T & q in {q} ) by FUNCT_2:def_1, TARSKI:def_1;
then A31: (dist (pmet1,p)) . q in (dist (pmet1,p)) .: {q} by FUNCT_1:def_6;
( not (dist (pmet1,p)) .: {q} is empty & (dist (pmet1,p)) .: {q} is bounded_below ) by A26, Lm1;
then (dist (pmet1,p)) . q > 0 by A31, A27, SEQ_4:def_2;
hence contradiction by A25, A29, A30, SEQFUNC:def_10; ::_thesis: verum
end;
pmet is_a_pseudometric_of the carrier of T by A2, A5, Th15;
then ( pmet is Reflexive & pmet is discerning & pmet is symmetric & pmet is triangle ) by A18, METRIC_1:def_3, NAGATA_1:def_10;
then A32: pmet is_metric_of the carrier of T by METRIC_6:3;
hence ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) by A5; ::_thesis: T is metrizable
for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
proof
let A be non empty Subset of T; ::_thesis: Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
set INF = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ;
A33: { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } or x in Cl A )
assume x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; ::_thesis: x in Cl A
then consider p being Point of T such that
A34: x = p and
A35: (lower_bound (pmet,A)) . p = 0 ;
A36: lower_bound ((dist (pmet,p)) .: A) = 0 by A35, Def3;
pmet is_a_pseudometric_of the carrier of T by A2, A5, Th15;
then A37: ( not (dist (pmet,p)) .: A is empty & (dist (pmet,p)) .: A is bounded_below ) by Lm1;
A38: ( A c= Cl A & ex y being set st y in A ) by PRE_TOPC:18, XBOOLE_0:def_1;
A39: A c= Cl A by PRE_TOPC:18;
assume not x in Cl A ; ::_thesis: contradiction
then consider n being Element of NAT such that
A40: for pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet1 holds
(lower_bound (pmet1,(Cl A))) . p > 0 by A3, A34, A38;
(1 / 2) |^ n > 0 by NEWTON:83;
then A41: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def_1;
(1 / 2) |^ n > 0 by NEWTON:83;
then A42: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def_1;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A43: FS2 . n = pmet1 and
A44: pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
set r = (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p);
A45: lower_bound ((dist (pmet1,p)) .: (Cl A)) = (lower_bound (pmet1,(Cl A))) . p by Def3;
A46: (lower_bound (pmet1,(Cl A))) . p > 0 by A40, A43;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) > 0 by A41, XREAL_1:129;
then ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 > 0 by XREAL_1:215;
then consider rn being real number such that
A47: rn in (dist (pmet,p)) .: A and
A48: rn < (lower_bound ((dist (pmet,p)) .: A)) + (((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2) by A37, SEQ_4:def_2;
consider a being set such that
A49: a in dom (dist (pmet,p)) and
A50: a in A and
A51: rn = (dist (pmet,p)) . a by A47, FUNCT_1:def_6;
reconsider a = a as Point of T by A49;
reconsider pa = [p,a] as Element of [: the carrier of T, the carrier of T:] ;
A52: (dist (pmet1,p)) . a = pmet1 . (p,a) by Def2;
dom (dist (pmet1,p)) = the carrier of T by FUNCT_2:def_1;
then A53: (dist (pmet1,p)) . a in (dist (pmet1,p)) .: (Cl A) by A50, A39, FUNCT_1:def_6;
( not (dist (pmet1,p)) .: (Cl A) is empty & (dist (pmet1,p)) .: (Cl A) is bounded_below ) by A44, A50, A39, Lm1;
then (lower_bound (pmet1,(Cl A))) . p <= (dist (pmet1,p)) . a by A53, A45, SEQ_4:def_2;
then (lower_bound (pmet1,(Cl A))) . p <= (FS2 # pa) . n by A43, A52, SEQFUNC:def_10;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) <= (((1 / 2) GeoSeq) . n) * ((FS2 # pa) . n) by A42, XREAL_1:64;
then A54: (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) <= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n by SEQ_1:8;
A55: for k being Element of NAT holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . k & (((1 / 2) GeoSeq) (#) (FS2 # pa)) . k <= (s (#) ((1 / 2) GeoSeq)) . k ) by A8;
pmet . pa = pmet . (p,a) ;
then A56: rn = pmet . pa by A51, Def2;
1 / 2 < 1 ;
then abs (1 / 2) < 1 by ABSVALUE:def_1;
then (1 / 2) GeoSeq is summable by SERIES_1:24;
then s (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then ((1 / 2) GeoSeq) (#) (FS2 # pa) is summable by A55, SERIES_1:20;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n <= Sum (((1 / 2) GeoSeq) (#) (FS2 # pa)) by A55, RSSPACE2:3;
then rn >= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n by A5, A56;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by A48, A36, XXREAL_0:2;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by A54, XXREAL_0:2;
hence contradiction by A41, A46, XREAL_1:129, XREAL_1:216; ::_thesis: verum
end;
Cl A c= { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } )
assume A57: x in Cl A ; ::_thesis: x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
then reconsider p = x as Point of T ;
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) by A2, A5, Th15;
then (lower_bound (pmet,A)) . p = 0 by A57, Th16;
hence x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; ::_thesis: verum
end;
hence Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } by A33, XBOOLE_0:def_10; ::_thesis: verum
end;
hence T is metrizable by A32, Th10; ::_thesis: verum
end;
theorem Th18: :: NAGATA_2:18
for D being non empty set
for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )
proof
let D be non empty set ; ::_thesis: for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )
let p, q be FinSequence of D; ::_thesis: for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )
let B be BinOp of D; ::_thesis: ( p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) implies ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) ) )
assume that
A1: p is one-to-one and
A2: q is one-to-one and
A3: rng q c= rng p and
A4: ( B is commutative & B is associative ) and
A5: ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) ; ::_thesis: ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )
A6: card (rng p) = len p by A1, FINSEQ_4:62;
consider r being FinSequence such that
A7: rng r = (rng p) \ (rng q) and
A8: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of D by A7, FINSEQ_1:def_4;
rng (q ^ r) = (rng q) \/ ((rng p) \ (rng q)) by A7, FINSEQ_1:31;
then A9: rng (q ^ r) = rng p by A3, XBOOLE_1:45;
rng r misses rng q by A7, XBOOLE_1:79;
then A10: q ^ r is one-to-one by A2, A8, FINSEQ_3:91;
then card (rng (q ^ r)) = len (q ^ r) by FINSEQ_4:62;
then ( len q < (len q) + (len r) or B is having_a_unity ) by A5, A9, A6, FINSEQ_1:22;
then A11: ( ( 1 <= len r & 1 <= len q & 1 <= len p ) or B is having_a_unity ) by A5, NAT_1:19, XXREAL_0:2;
ex P being Permutation of (dom p) st
( p * P = q ^ r & dom P = dom p & rng P = dom p ) by A1, A10, A9, BHSP_5:1;
then A12: B "**" p = B "**" (q ^ r) by A4, A11, FINSOP_1:7;
B "**" (q ^ r) = B . ((B "**" q),(B "**" r)) by A4, A11, FINSOP_1:5;
hence ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) ) by A7, A8, A12; ::_thesis: verum
end;
registration
let T1, T2 be TopSpace;
let f be RealMap of [:T1,T2:];
let t1 be Point of T1;
let t2 be Point of T2;
clusterf . (t1,t2) -> real ;
coherence
f . (t1,t2) is real ;
end;
Lm2: PairFunc " = PairFunc "
by Th2, TOPS_2:def_4;
theorem Th19: :: NAGATA_2:19
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
proof
let T be non empty TopSpace; ::_thesis: ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
thus ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is metrizable ) ::_thesis: ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) )
proof
set cTT = the carrier of [:T,T:];
set bcT = bool the carrier of T;
set cT = the carrier of T;
assume that
A1: T is regular and
A2: T is T_1 and
A3: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ; ::_thesis: T is metrizable
set Fun = Funcs ( the carrier of [:T,T:],REAL);
consider Bn being FamilySequence of T such that
A4: Bn is Basis_sigma_locally_finite by A3;
defpred S1[ set , set , RealMap of [:T,T:]] means ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( $3 = pmet & $3 is continuous & pmet is_a_pseudometric_of the carrier of T & ( for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . $2 & B in Bn . $1 & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) ) );
defpred S2[ set , set ] means ex F being RealMap of [:T,T:] st
( F = $2 & ( for n, m being Element of NAT st (PairFunc ") . $1 = [n,m] holds
S1[n,m,F] ) );
A5: Union Bn is Basis of T by A4, NAGATA_1:def_6;
A6: Bn is sigma_locally_finite by A4, NAGATA_1:def_6;
A7: for n, m being Element of NAT ex pmet9 being RealMap of [:T,T:] st S1[n,m,pmet9]
proof
defpred S3[ Element of Funcs ( the carrier of [:T,T:],REAL), Element of Funcs ( the carrier of [:T,T:],REAL), set ] means $1 + $2 = $3;
defpred S4[ RealMap of T, Function] means for p, q being Point of T holds $2 . (p,q) = abs (($1 . p) - ($1 . q));
let n, m be Element of NAT ; ::_thesis: ex pmet9 being RealMap of [:T,T:] st S1[n,m,pmet9]
deffunc H1( set ) -> set = union { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= $1 ) } ;
set Bnn = Bn . n;
deffunc H2( Subset of T) -> set = { Q where Q is Subset of T : ( Q in Bn . n & Q meets $1 ) } ;
defpred S5[ set , Subset of T] means ( $1 in $2 & $2 is open & H2($2) is finite );
A8: for A being set st A in bool the carrier of T holds
H1(A) in bool the carrier of T
proof
let A be set ; ::_thesis: ( A in bool the carrier of T implies H1(A) in bool the carrier of T )
assume A in bool the carrier of T ; ::_thesis: H1(A) in bool the carrier of T
set Um = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ;
now__::_thesis:_for_uv_being_set_st_uv_in_H1(A)_holds_
uv_in_the_carrier_of_T
let uv be set ; ::_thesis: ( uv in H1(A) implies uv in the carrier of T )
assume uv in H1(A) ; ::_thesis: uv in the carrier of T
then consider v being set such that
A9: uv in v and
A10: v in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } by TARSKI:def_4;
ex B being Subset of T st
( v = B & B in Bn . m & Cl B c= A ) by A10;
hence uv in the carrier of T by A9; ::_thesis: verum
end;
then H1(A) c= the carrier of T by TARSKI:def_3;
hence H1(A) in bool the carrier of T ; ::_thesis: verum
end;
consider Vm being Function of (bool the carrier of T),(bool the carrier of T) such that
A11: for A being set st A in bool the carrier of T holds
Vm . A = H1(A) from FUNCT_2:sch_2(A8);
defpred S6[ set , set ] means ex F being RealMap of T ex S being Subset of T st
( S = $1 & F = $2 & F is continuous & ( for p being Point of T holds
( 0 <= F . p & F . p <= 1 & ( p in S ` implies F . p = 0 ) & ( p in Cl (Vm . S) implies F . p = 1 ) ) ) );
A12: Bn . m is locally_finite by A6, NAGATA_1:def_3;
A13: for A being Subset of T holds Cl (Vm . A) c= A
proof
let A be Subset of T; ::_thesis: Cl (Vm . A) c= A
set VmA = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ;
{ Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } c= bool the carrier of T
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } or B in bool the carrier of T )
assume B in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ; ::_thesis: B in bool the carrier of T
then ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) ;
hence B in bool the carrier of T ; ::_thesis: verum
end;
then reconsider VmA = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } as Subset-Family of T ;
A14: union (clf VmA) c= A
proof
let ClBu be set ; :: according to TARSKI:def_3 ::_thesis: ( not ClBu in union (clf VmA) or ClBu in A )
assume ClBu in union (clf VmA) ; ::_thesis: ClBu in A
then consider ClB being set such that
A15: ClBu in ClB and
A16: ClB in clf VmA by TARSKI:def_4;
reconsider ClB = ClB as Subset of T by A16;
consider B being Subset of T such that
A17: Cl B = ClB and
A18: B in VmA by A16, PCOMPS_1:def_2;
ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) by A18;
hence ClBu in A by A15, A17; ::_thesis: verum
end;
VmA c= Bn . m
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in VmA or B in Bn . m )
assume B in VmA ; ::_thesis: B in Bn . m
then ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) ;
hence B in Bn . m ; ::_thesis: verum
end;
then Cl (union VmA) = union (clf VmA) by A12, PCOMPS_1:9, PCOMPS_1:20;
hence Cl (Vm . A) c= A by A11, A14; ::_thesis: verum
end;
A19: for A being set st A in Bn . n holds
ex f being set st
( f in Funcs ( the carrier of T,REAL) & S6[A,f] )
proof
let A be set ; ::_thesis: ( A in Bn . n implies ex f being set st
( f in Funcs ( the carrier of T,REAL) & S6[A,f] ) )
assume A in Bn . n ; ::_thesis: ex f being set st
( f in Funcs ( the carrier of T,REAL) & S6[A,f] )
then A20: A in Union Bn by PROB_1:12;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider A = A as open Subset of T by A20, PRE_TOPC:def_2;
A ` misses A by XBOOLE_1:79;
then A21: A ` misses Cl (Vm . A) by A13, XBOOLE_1:63;
T is normal by A1, A4, NAGATA_1:20;
then consider f being Function of T,R^1 such that
A22: ( f is continuous & ( for p being Point of T holds
( 0 <= f . p & f . p <= 1 & ( p in A ` implies f . p = 0 ) & ( p in Cl (Vm . A) implies f . p = 1 ) ) ) ) by A21, URYSOHN3:20;
reconsider f9 = f as RealMap of T by TOPMETR:17;
A23: ex F being RealMap of T ex S being Subset of T st
( S = A & F = f9 & F is continuous & ( for p being Point of T holds
( 0 <= F . p & F . p <= 1 & ( p in S ` implies F . p = 0 ) & ( p in Cl (Vm . S) implies F . p = 1 ) ) ) )
proof
take f9 ; ::_thesis: ex S being Subset of T st
( S = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds
( 0 <= f9 . p & f9 . p <= 1 & ( p in S ` implies f9 . p = 0 ) & ( p in Cl (Vm . S) implies f9 . p = 1 ) ) ) )
take A ; ::_thesis: ( A = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds
( 0 <= f9 . p & f9 . p <= 1 & ( p in A ` implies f9 . p = 0 ) & ( p in Cl (Vm . A) implies f9 . p = 1 ) ) ) )
thus ( A = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds
( 0 <= f9 . p & f9 . p <= 1 & ( p in A ` implies f9 . p = 0 ) & ( p in Cl (Vm . A) implies f9 . p = 1 ) ) ) ) by A22, JORDAN5A:27; ::_thesis: verum
end;
f9 in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
hence ex f being set st
( f in Funcs ( the carrier of T,REAL) & S6[A,f] ) by A23; ::_thesis: verum
end;
consider Fn being Function of (Bn . n),(Funcs ( the carrier of T,REAL)) such that
A24: for A being set st A in Bn . n holds
S6[A,Fn . A] from FUNCT_2:sch_1(A19);
Bn . n is locally_finite by A6, NAGATA_1:def_3;
then A25: for p being Element of the carrier of T ex A being Element of bool the carrier of T st S5[p,A] by PCOMPS_1:def_1;
consider Sx being Function of the carrier of T,(bool the carrier of T) such that
A26: for p being Element of the carrier of T holds S5[p,Sx . p] from FUNCT_2:sch_3(A25);
defpred S7[ set , set ] means for x, y being Element of T st $1 = [x,y] holds
$2 = [:(Sx . x),(Sx . y):];
A27: for pq9 being set st pq9 in the carrier of [:T,T:] holds
ex SS being set st
( SS in bool the carrier of [:T,T:] & S7[pq9,SS] )
proof
let pq9 be set ; ::_thesis: ( pq9 in the carrier of [:T,T:] implies ex SS being set st
( SS in bool the carrier of [:T,T:] & S7[pq9,SS] ) )
assume pq9 in the carrier of [:T,T:] ; ::_thesis: ex SS being set st
( SS in bool the carrier of [:T,T:] & S7[pq9,SS] )
then pq9 in [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then consider p, q being set such that
A28: ( p in the carrier of T & q in the carrier of T ) and
A29: pq9 = [p,q] by ZFMISC_1:def_2;
reconsider p = p, q = q as Point of T by A28;
now__::_thesis:_for_p1,_q1_being_Point_of_T_st_pq9_=_[p1,q1]_holds_
[:(Sx_._p),(Sx_._q):]_=_[:(Sx_._p1),(Sx_._q1):]
let p1, q1 be Point of T; ::_thesis: ( pq9 = [p1,q1] implies [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] )
assume A30: pq9 = [p1,q1] ; ::_thesis: [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]
then p1 = p by A29, XTUPLE_0:1;
hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] by A29, A30, XTUPLE_0:1; ::_thesis: verum
end;
hence ex SS being set st
( SS in bool the carrier of [:T,T:] & S7[pq9,SS] ) ; ::_thesis: verum
end;
consider SS being Function of the carrier of [:T,T:],(bool the carrier of [:T,T:]) such that
A31: for pq being set st pq in the carrier of [:T,T:] holds
S7[pq,SS . pq] from FUNCT_2:sch_1(A27);
A32: for pq9 being Point of [:T,T:] holds
( pq9 in SS . pq9 & SS . pq9 is open )
proof
let pq9 be Point of [:T,T:]; ::_thesis: ( pq9 in SS . pq9 & SS . pq9 is open )
pq9 in the carrier of [:T,T:] ;
then pq9 in [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then consider p, q being set such that
A33: ( p in the carrier of T & q in the carrier of T ) and
A34: pq9 = [p,q] by ZFMISC_1:def_2;
reconsider p = p, q = q as Point of T by A33;
A35: ( p in Sx . p & q in Sx . q ) by A26;
A36: ( Sx . p is open & Sx . q is open ) by A26;
SS . pq9 = [:(Sx . p),(Sx . q):] by A31, A34;
hence ( pq9 in SS . pq9 & SS . pq9 is open ) by A34, A35, A36, BORSUK_1:6, ZFMISC_1:def_2; ::_thesis: verum
end;
A37: for f, g being Element of Funcs ( the carrier of [:T,T:],REAL) ex fg being Element of Funcs ( the carrier of [:T,T:],REAL) st S3[f,g,fg]
proof
let f, g be Element of Funcs ( the carrier of [:T,T:],REAL); ::_thesis: ex fg being Element of Funcs ( the carrier of [:T,T:],REAL) st S3[f,g,fg]
set f9 = f;
set g9 = g;
f + g in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
hence ex fg being Element of Funcs ( the carrier of [:T,T:],REAL) st S3[f,g,fg] ; ::_thesis: verum
end;
consider ADD being BinOp of (Funcs ( the carrier of [:T,T:],REAL)) such that
A38: for f, g being Element of Funcs ( the carrier of [:T,T:],REAL) holds S3[f,g,ADD . (f,g)] from BINOP_1:sch_3(A37);
A39: for f being Element of Funcs ( the carrier of T,REAL) ex fxy being Element of Funcs ( the carrier of [:T,T:],REAL) st S4[f,fxy]
proof
let f be Element of Funcs ( the carrier of T,REAL); ::_thesis: ex fxy being Element of Funcs ( the carrier of [:T,T:],REAL) st S4[f,fxy]
defpred S8[ Element of T, Element of T, set ] means $3 = abs ((f . $1) - (f . $2));
A40: for x, y being Element of the carrier of T ex r being Element of REAL st S8[x,y,r] ;
consider Fd being Function of [: the carrier of T, the carrier of T:],REAL such that
A41: for x, y being Element of the carrier of T holds S8[x,y,Fd . (x,y)] from BINOP_1:sch_3(A40);
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def_2;
then Fd in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
hence ex fxy being Element of Funcs ( the carrier of [:T,T:],REAL) st S4[f,fxy] by A41; ::_thesis: verum
end;
consider Fdist being Function of (Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)) such that
A42: for fd being Element of Funcs ( the carrier of T,REAL) holds S4[fd,Fdist . fd] from FUNCT_2:sch_3(A39);
deffunc H3( Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & A in H2(Sx . $1) ) } ;
deffunc H4( set ) -> set = { (Fdist . fd) where fd is RealMap of T : fd in $1 } ;
defpred S8[ set , Function] means ( $2 is one-to-one & ex p, q being Point of T st
( [p,q] = $1 & rng $2 = H4(H3(p) \/ H3(q)) ) );
A43: for p being Point of T holds H3(p) is finite
proof
deffunc H5( Subset of T) -> set = Fn . $1;
let p be Point of T; ::_thesis: H3(p) is finite
set SFxx = { H5(A) where A is Subset of T : A in H2(Sx . p) } ;
A44: H3(p) c= { H5(A) where A is Subset of T : A in H2(Sx . p) }
proof
let FA be set ; :: according to TARSKI:def_3 ::_thesis: ( not FA in H3(p) or FA in { H5(A) where A is Subset of T : A in H2(Sx . p) } )
assume FA in H3(p) ; ::_thesis: FA in { H5(A) where A is Subset of T : A in H2(Sx . p) }
then ex A being Subset of T st
( FA = Fn . A & A in Bn . n & A in H2(Sx . p) ) ;
hence FA in { H5(A) where A is Subset of T : A in H2(Sx . p) } ; ::_thesis: verum
end;
A45: H2(Sx . p) is finite by A26;
{ H5(A) where A is Subset of T : A in H2(Sx . p) } is finite from FRAENKEL:sch_21(A45);
hence H3(p) is finite by A44; ::_thesis: verum
end;
A46: for p, q being Point of T holds
( H4(H3(p) \/ H3(q)) is finite & H4(H3(p) \/ H3(q)) c= Funcs ( the carrier of [:T,T:],REAL) )
proof
deffunc H5( RealMap of T) -> set = Fdist . $1;
let p, q be Point of T; ::_thesis: ( H4(H3(p) \/ H3(q)) is finite & H4(H3(p) \/ H3(q)) c= Funcs ( the carrier of [:T,T:],REAL) )
A47: H4(H3(p) \/ H3(q)) c= Funcs ( the carrier of [:T,T:],REAL)
proof
let FDm be set ; :: according to TARSKI:def_3 ::_thesis: ( not FDm in H4(H3(p) \/ H3(q)) or FDm in Funcs ( the carrier of [:T,T:],REAL) )
assume FDm in H4(H3(p) \/ H3(q)) ; ::_thesis: FDm in Funcs ( the carrier of [:T,T:],REAL)
then consider fd being RealMap of T such that
A48: FDm = Fdist . fd and
fd in H3(p) \/ H3(q) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
hence FDm in Funcs ( the carrier of [:T,T:],REAL) by A48, FUNCT_2:5; ::_thesis: verum
end;
set RNG9 = { H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) } ;
A49: H4(H3(p) \/ H3(q)) c= { H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) }
proof
let Fdistfd be set ; :: according to TARSKI:def_3 ::_thesis: ( not Fdistfd in H4(H3(p) \/ H3(q)) or Fdistfd in { H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) } )
assume Fdistfd in H4(H3(p) \/ H3(q)) ; ::_thesis: Fdistfd in { H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) }
then consider fd being RealMap of T such that
A50: ( Fdistfd = Fdist . fd & fd in H3(p) \/ H3(q) ) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
hence Fdistfd in { H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) } by A50; ::_thesis: verum
end;
( H3(p) is finite & H3(q) is finite ) by A43;
then A51: H3(p) \/ H3(q) is finite ;
{ H5(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H3(p) \/ H3(q) } is finite from FRAENKEL:sch_21(A51);
hence ( H4(H3(p) \/ H3(q)) is finite & H4(H3(p) \/ H3(q)) c= Funcs ( the carrier of [:T,T:],REAL) ) by A47, A49; ::_thesis: verum
end;
A52: for pq being Element of the carrier of [:T,T:] ex G being Element of (Funcs ( the carrier of [:T,T:],REAL)) * st S8[pq,G]
proof
let pq be Element of the carrier of [:T,T:]; ::_thesis: ex G being Element of (Funcs ( the carrier of [:T,T:],REAL)) * st S8[pq,G]
pq in the carrier of [:T,T:] ;
then pq in [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then consider p, q being set such that
A53: ( p in the carrier of T & q in the carrier of T ) and
A54: pq = [p,q] by ZFMISC_1:def_2;
reconsider p = p, q = q as Point of T by A53;
consider SF being FinSequence such that
A55: rng SF = H4(H3(p) \/ H3(q)) and
A56: SF is one-to-one by A46, FINSEQ_4:58;
rng SF c= Funcs ( the carrier of [:T,T:],REAL) by A46, A55;
then reconsider SF = SF as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_4;
SF in (Funcs ( the carrier of [:T,T:],REAL)) * by FINSEQ_1:def_11;
hence ex G being Element of (Funcs ( the carrier of [:T,T:],REAL)) * st S8[pq,G] by A54, A55, A56; ::_thesis: verum
end;
consider SFdist being Function of the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *) such that
A57: for pq being Element of the carrier of [:T,T:] holds S8[pq,SFdist . pq] from FUNCT_2:sch_3(A52);
defpred S9[ set , set ] means for FS being FinSequence of Funcs ( the carrier of [:T,T:],REAL) st FS = SFdist . $1 holds
$2 = ADD "**" FS;
A58: for pq being set st pq in the carrier of [:T,T:] holds
ex S being set st
( S in Funcs ( the carrier of [:T,T:],REAL) & S9[pq,S] )
proof
let pq be set ; ::_thesis: ( pq in the carrier of [:T,T:] implies ex S being set st
( S in Funcs ( the carrier of [:T,T:],REAL) & S9[pq,S] ) )
assume pq in the carrier of [:T,T:] ; ::_thesis: ex S being set st
( S in Funcs ( the carrier of [:T,T:],REAL) & S9[pq,S] )
then SFdist . pq in (Funcs ( the carrier of [:T,T:],REAL)) * by FUNCT_2:5;
then reconsider SF = SFdist . pq as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
for FS being FinSequence of Funcs ( the carrier of [:T,T:],REAL) st FS = SFdist . pq holds
ADD "**" FS = ADD "**" SF ;
hence ex S being set st
( S in Funcs ( the carrier of [:T,T:],REAL) & S9[pq,S] ) ; ::_thesis: verum
end;
consider SumFdist being Function of the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)) such that
A59: for xy being set st xy in the carrier of [:T,T:] holds
S9[xy,SumFdist . xy] from FUNCT_2:sch_1(A58);
reconsider SumFdist9 = SumFdist as Function of the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:], the carrier of R^1)) by TOPMETR:17;
reconsider SumFTS9 = SumFdist9 Toler as RealMap of [:T,T:] by TOPMETR:17;
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then reconsider SumFTS = SumFdist9 Toler as Function of [: the carrier of T, the carrier of T:],REAL by TOPMETR:17;
A60: for f1, f2 being RealMap of [:T,T:] holds ADD . (f1,f2) = f1 + f2
proof
let f1, f2 be RealMap of [:T,T:]; ::_thesis: ADD . (f1,f2) = f1 + f2
reconsider f19 = f1, f29 = f2 as Element of Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
ADD . (f19,f29) = f19 + f29 by A38;
hence ADD . (f1,f2) = f1 + f2 ; ::_thesis: verum
end;
A61: for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
SumFTS9 . [p,q] >= 1
proof
let p, q be Point of T; ::_thesis: ( ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies SumFTS9 . [p,q] >= 1 )
assume ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; ::_thesis: SumFTS9 . [p,q] >= 1
then consider A, B being Subset of T such that
A is open and
B is open and
A62: A in Bn . m and
A63: B in Bn . n and
A64: p in A and
A65: Cl A c= B and
A66: not q in B ;
A67: S6[B,Fn . B] by A24, A63;
A in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= B ) } by A62, A65;
then A c= H1(B) by ZFMISC_1:74;
then A68: A c= Vm . B by A11;
Vm . B c= Cl (Vm . B) by PRE_TOPC:18;
then A69: p in Cl (Vm . B) by A64, A68, TARSKI:def_3;
( Cl (Vm . B) c= B & p in Sx . p ) by A13, A26;
then Sx . p meets B by A69, XBOOLE_0:3;
then A70: B in H2(Sx . p) by A63;
reconsider pq = [p,q] as Point of [:T,T:] by BORSUK_1:def_2;
reconsider SF = SFdist . pq as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
consider x, y being Point of T such that
A71: [x,y] = pq and
A72: rng SF = H4(H3(x) \/ H3(y)) by A57;
reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:66;
assume A73: SumFTS9 . [p,q] < 1 ; ::_thesis: contradiction
reconsider FnB = Fn . B as RealMap of T by A63, FUNCT_2:5, FUNCT_2:66;
A74: FnB in Funcs ( the carrier of T,REAL) by A63, FUNCT_2:5;
q in B ` by A66, XBOOLE_0:def_5;
then A75: FnB . q = 0 by A67;
x = p by A71, XTUPLE_0:1;
then FnB in H3(x) by A63, A70;
then FnB in H3(x) \/ H3(y) by XBOOLE_0:def_3;
then A76: Fdist . FnB in rng SF by A72;
then reconsider FdistFnB = Fdist . FnB as RealMap of [:T,T:] by FUNCT_2:66;
SF <> {} by A76, RELAT_1:38;
then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A77: F . 1 = SF . 1 and
A78: for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A79: ADD "**" SF = F . (len SF) by FINSOP_1:def_1;
A80: ( SumFTS . pq = (SumFdist . pq) . pq & SumFdist . pq = ASF ) by A59, NAGATA_1:def_8;
defpred S10[ Element of NAT ] means for k being Element of NAT st k <> 0 & k <= $1 & $1 <= len SF holds
for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . $1 holds
fk . pq <= Fn . pq;
A81: for k being Element of NAT st k <> 0 & k <= len SF holds
for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0
proof
let k be Element of NAT ; ::_thesis: ( k <> 0 & k <= len SF implies for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0 )
assume that
A82: k <> 0 and
A83: k <= len SF ; ::_thesis: for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0
k >= 1 by A82, NAT_1:14;
then k in dom SF by A83, FINSEQ_3:25;
then SF . k in H4(H3(x) \/ H3(y)) by A72, FUNCT_1:def_3;
then consider fd being RealMap of T such that
A84: Fdist . fd = SF . k and
fd in H3(x) \/ H3(y) ;
let f be RealMap of [:T,T:]; ::_thesis: ( f = SF . k implies f . pq >= 0 )
assume A85: f = SF . k ; ::_thesis: f . pq >= 0
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then f . (p,q) = abs ((fd . p) - (fd . q)) by A42, A85, A84;
hence f . pq >= 0 by COMPLEX1:46; ::_thesis: verum
end;
A86: for i being Element of NAT st S10[i] holds
S10[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S10[i] implies S10[i + 1] )
assume A87: S10[i] ; ::_thesis: S10[i + 1]
let k be Element of NAT ; ::_thesis: ( k <> 0 & k <= i + 1 & i + 1 <= len SF implies for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq )
assume that
A88: k <> 0 and
A89: k <= i + 1 and
A90: i + 1 <= len SF ; ::_thesis: for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq
now__::_thesis:_for_fk,_Fn_being_RealMap_of_[:T,T:]_st_fk_=_SF_._k_&_Fn_=_F_._(i_+_1)_holds_
fk_._pq_<=_Fn_._pq
1 <= i + 1 by NAT_1:14;
then i + 1 in dom SF by A90, FINSEQ_3:25;
then SF . (i + 1) in rng SF by FUNCT_1:def_3;
then reconsider SFi1 = SF . (i + 1) as RealMap of [:T,T:] by FUNCT_2:66;
reconsider Fi = F . i as RealMap of [:T,T:] by FUNCT_2:66;
let fk, Fn be RealMap of [:T,T:]; ::_thesis: ( fk = SF . k & Fn = F . (i + 1) implies b1 . pq <= b2 . pq )
assume that
A91: fk = SF . k and
A92: Fn = F . (i + 1) ; ::_thesis: b1 . pq <= b2 . pq
percases ( k < i + 1 or k = i + 1 ) by A89, XXREAL_0:1;
supposeA93: k < i + 1 ; ::_thesis: b1 . pq <= b2 . pq
A94: i < len SF by A90, NAT_1:13;
i <> 0 by A88, A93, NAT_1:13;
then F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A78, A94;
then A95: Fn = Fi + SFi1 by A60, A92;
SFi1 . pq >= 0 by A81, A90;
then (Fi . pq) + 0 <= (Fi . pq) + (SFi1 . pq) by XREAL_1:7;
then A96: Fn . pq >= Fi . pq by A95, NAGATA_1:def_7;
A97: i <= len SF by A90, NAT_1:13;
k <= i by A93, NAT_1:13;
then fk . pq <= Fi . pq by A87, A88, A91, A97;
hence fk . pq <= Fn . pq by A96, XXREAL_0:2; ::_thesis: verum
end;
supposeA98: k = i + 1 ; ::_thesis: b1 . pq <= b2 . pq
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: b1 . pq <= b2 . pq
hence fk . pq <= Fn . pq by A77, A91, A92, A98; ::_thesis: verum
end;
supposeA99: i <> 0 ; ::_thesis: b1 . pq <= b2 . pq
i + 0 < i + 1 by XREAL_1:8;
then A100: i < len SF by A90, XXREAL_0:2;
1 <= i by A99, NAT_1:14;
then i in dom SF by A100, FINSEQ_3:25;
then SF . i in rng SF by FUNCT_1:def_3;
then reconsider SFi = SF . i as RealMap of [:T,T:] by FUNCT_2:66;
0 <= SFi . pq by A81, A99, A100;
then 0 <= Fi . pq by A87, A99, A100;
then A101: (Fi . pq) + (fk . pq) >= 0 + (fk . pq) by XREAL_1:7;
F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A78, A99, A100;
then Fn = Fi + fk by A60, A91, A92, A98;
hence fk . pq <= Fn . pq by A101, NAGATA_1:def_7; ::_thesis: verum
end;
end;
end;
end;
end;
hence for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq ; ::_thesis: verum
end;
A102: S10[ 0 ] ;
A103: for i being Element of NAT holds S10[i] from NAT_1:sch_1(A102, A86);
consider k being set such that
A104: k in dom SF and
A105: SF . k = Fdist . FnB by A76, FUNCT_1:def_3;
A106: k in Seg (len SF) by A104, FINSEQ_1:def_3;
FnB . p = 1 by A69, A67;
then A107: FdistFnB . (p,q) = abs (1 - 0) by A42, A74, A75;
reconsider k = k as Element of NAT by A104;
A108: abs 1 = 1 by ABSVALUE:def_1;
( k <> 0 & k <= len SF ) by A106, FINSEQ_1:1;
hence contradiction by A73, A80, A79, A103, A107, A108, A105; ::_thesis: verum
end;
A109: now__::_thesis:_for_p,_q_being_Point_of_T_st_ex_A,_B_being_Subset_of_T_st_
(_A_is_open_&_B_is_open_&_A_in_Bn_._m_&_B_in_Bn_._n_&_p_in_A_&_Cl_A_c=_B_&_not_q_in_B_)_holds_
1_=_(min_(1,SumFTS9))_._[p,q]
let p, q be Point of T; ::_thesis: ( ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies 1 = (min (1,SumFTS9)) . [p,q] )
assume ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; ::_thesis: 1 = (min (1,SumFTS9)) . [p,q]
then SumFTS9 . [p,q] >= 1 by A61;
then A110: 1 = min (1,(SumFTS9 . [p,q])) by XXREAL_0:def_9;
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def_2;
hence 1 = (min (1,SumFTS9)) . [p,q] by A110, NAGATA_1:def_9; ::_thesis: verum
end;
A111: for pq being Element of the carrier of [:T,T:]
for map9 being Element of Funcs ( the carrier of [:T,T:],REAL) st map9 is_a_unity_wrt ADD holds
map9 . pq = 0
proof
let pq be Element of the carrier of [:T,T:]; ::_thesis: for map9 being Element of Funcs ( the carrier of [:T,T:],REAL) st map9 is_a_unity_wrt ADD holds
map9 . pq = 0
let map9 be Element of Funcs ( the carrier of [:T,T:],REAL); ::_thesis: ( map9 is_a_unity_wrt ADD implies map9 . pq = 0 )
assume map9 is_a_unity_wrt ADD ; ::_thesis: map9 . pq = 0
then ADD . (map9,map9) = map9 by BINOP_1:3;
then (map9 + map9) . pq = map9 . pq by A38;
then (map9 . pq) + (map9 . pq) = map9 . pq by NAGATA_1:def_7;
hence map9 . pq = 0 ; ::_thesis: verum
end;
A112: for pq1, pq2 being Point of [:T,T:] holds
( ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) & ( for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ) )
proof
deffunc H5( Element of T, Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & ( for FnA being RealMap of T holds
( not Fn . A = FnA or FnA . $1 > 0 or FnA . $2 > 0 ) ) ) } ;
let pq1, pq2 be Point of [:T,T:]; ::_thesis: ( ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) & ( for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ) )
reconsider S1 = SFdist . pq1, S2 = SFdist . pq2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
consider p1, q1 being Point of T such that
A113: [p1,q1] = pq1 and
A114: rng S1 = H4(H3(p1) \/ H3(q1)) by A57;
A115: for p, q, p1, q1 being Point of T st [p,q] in SS . [p1,q1] holds
H5(p,q) c= H3(p1) \/ H3(q1)
proof
let p, q, p1, q1 be Point of T; ::_thesis: ( [p,q] in SS . [p1,q1] implies H5(p,q) c= H3(p1) \/ H3(q1) )
assume A116: [p,q] in SS . [p1,q1] ; ::_thesis: H5(p,q) c= H3(p1) \/ H3(q1)
reconsider pq1 = [p1,q1] as Element of the carrier of [:T,T:] by BORSUK_1:def_2;
[:(Sx . p1),(Sx . q1):] = SS . pq1 by A31;
then A117: ( p in Sx . p1 & q in Sx . q1 ) by A116, ZFMISC_1:87;
let no0 be set ; :: according to TARSKI:def_3 ::_thesis: ( not no0 in H5(p,q) or no0 in H3(p1) \/ H3(q1) )
assume no0 in H5(p,q) ; ::_thesis: no0 in H3(p1) \/ H3(q1)
then consider A being Subset of T such that
A118: no0 = Fn . A and
A119: A in Bn . n and
A120: for FnA being RealMap of T holds
( not Fn . A = FnA or FnA . p > 0 or FnA . q > 0 ) ;
reconsider FnA = Fn . A as RealMap of T by A119, FUNCT_2:5, FUNCT_2:66;
A121: ( FnA . p > 0 or FnA . q > 0 ) by A120;
S6[A,Fn . A] by A24, A119;
then ( not p in the carrier of T \ A or not q in the carrier of T \ A ) by A121;
then ( p in A or q in A ) by XBOOLE_0:def_5;
then ( A meets Sx . p1 or A meets Sx . q1 ) by A117, XBOOLE_0:3;
then ( A in H2(Sx . p1) or A in H2(Sx . q1) ) by A119;
then ( FnA in H3(p1) or FnA in H3(q1) ) by A119;
hence no0 in H3(p1) \/ H3(q1) by A118, XBOOLE_0:def_3; ::_thesis: verum
end;
A122: H4(H5(p1,q1)) c= H4(H3(p1) \/ H3(q1))
proof
( p1 in Sx . p1 & q1 in Sx . q1 ) by A26;
then [p1,q1] in [:(Sx . p1),(Sx . q1):] by ZFMISC_1:87;
then [p1,q1] in SS . [p1,q1] by A31;
then A123: H5(p1,q1) c= H3(p1) \/ H3(q1) by A115;
let FD be set ; :: according to TARSKI:def_3 ::_thesis: ( not FD in H4(H5(p1,q1)) or FD in H4(H3(p1) \/ H3(q1)) )
assume FD in H4(H5(p1,q1)) ; ::_thesis: FD in H4(H3(p1) \/ H3(q1))
then ex fd being RealMap of T st
( FD = Fdist . fd & fd in H5(p1,q1) ) ;
hence FD in H4(H3(p1) \/ H3(q1)) by A123; ::_thesis: verum
end;
A124: for f being FinSequence of Funcs ( the carrier of [:T,T:],REAL)
for p, q, p1, q1 being Point of T st rng f = H4(H3(p1) \/ H3(q1)) \ H4(H5(p,q)) holds
(ADD "**" f) . [p,q] = 0
proof
let f be FinSequence of Funcs ( the carrier of [:T,T:],REAL); ::_thesis: for p, q, p1, q1 being Point of T st rng f = H4(H3(p1) \/ H3(q1)) \ H4(H5(p,q)) holds
(ADD "**" f) . [p,q] = 0
let p, q, p1, q1 be Point of T; ::_thesis: ( rng f = H4(H3(p1) \/ H3(q1)) \ H4(H5(p,q)) implies (ADD "**" f) . [p,q] = 0 )
assume A125: rng f = H4(H3(p1) \/ H3(q1)) \ H4(H5(p,q)) ; ::_thesis: (ADD "**" f) . [p,q] = 0
reconsider pq = [p,q] as Element of the carrier of [:T,T:] by BORSUK_1:def_2;
now__::_thesis:_(ADD_"**"_f)_._pq_=_0
percases ( len f = 0 or len f <> 0 ) ;
supposeA126: len f = 0 ; ::_thesis: (ADD "**" f) . pq = 0
A127: ADD is having_a_unity by A60, NAGATA_1:23;
then A128: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def_2;
ADD "**" f = the_unity_wrt ADD by A126, A127, FINSOP_1:def_1;
then ADD "**" f is_a_unity_wrt ADD by A128, BINOP_1:def_8;
hence (ADD "**" f) . pq = 0 by A111; ::_thesis: verum
end;
supposeA129: len f <> 0 ; ::_thesis: (ADD "**" f) . pq = 0
then len f >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A130: F . 1 = f . 1 and
A131: for n being Element of NAT st 0 <> n & n < len f holds
F . (n + 1) = ADD . ((F . n),(f . (n + 1))) and
A132: ADD "**" f = F . (len f) by FINSOP_1:def_1;
defpred S10[ Element of NAT ] means ( $1 <> 0 & $1 <= len f implies (F . $1) . pq = 0 );
A133: for k being Element of NAT st S10[k] holds
S10[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S10[k] implies S10[k + 1] )
assume A134: S10[k] ; ::_thesis: S10[k + 1]
assume that
k + 1 <> 0 and
A135: k + 1 <= len f ; ::_thesis: (F . (k + 1)) . pq = 0
A136: k < len f by A135, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom f by A135, FINSEQ_3:25;
then A137: f . (k + 1) in H4(H3(p1) \/ H3(q1)) \ H4(H5(p,q)) by A125, FUNCT_1:def_3;
then f . (k + 1) in H4(H3(p1) \/ H3(q1)) ;
then consider fd being RealMap of T such that
A138: Fdist . fd = f . (k + 1) and
A139: fd in H3(p1) \/ H3(q1) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, fk1 = f . (k + 1) as RealMap of [:T,T:] by A138, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A140: Fdistfd . (p,q) = abs ((fd . p) - (fd . q)) by A42;
A141: not f . (k + 1) in H4(H5(p,q)) by A137, XBOOLE_0:def_5;
A142: ( fd . p = 0 & fd . q = 0 )
proof
assume A143: ( fd . p <> 0 or fd . q <> 0 ) ; ::_thesis: contradiction
percases ( fd in H3(p1) or fd in H3(q1) ) by A139, XBOOLE_0:def_3;
suppose fd in H3(p1) ; ::_thesis: contradiction
then consider A being Subset of T such that
A144: fd = Fn . A and
A145: A in Bn . n and
A in H2(Sx . p1) ;
A146: S6[A,Fn . A] by A24, A145;
not fd in H5(p,q) by A141, A138;
then ex FnA being RealMap of T st
( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A144, A145;
hence contradiction by A143, A144, A146; ::_thesis: verum
end;
suppose fd in H3(q1) ; ::_thesis: contradiction
then consider A being Subset of T such that
A147: fd = Fn . A and
A148: A in Bn . n and
A in H2(Sx . q1) ;
A149: S6[A,Fn . A] by A24, A148;
not fd in H5(p,q) by A141, A138;
then ex FnA being RealMap of T st
( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A147, A148;
hence contradiction by A143, A147, A149; ::_thesis: verum
end;
end;
end;
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: (F . (k + 1)) . pq = 0
hence (F . (k + 1)) . pq = 0 by A130, A138, A142, A140, ABSVALUE:2; ::_thesis: verum
end;
supposeA150: k > 0 ; ::_thesis: (F . (k + 1)) . pq = 0
then Fk1 = ADD . (Fk,fk1) by A131, A136;
then Fk1 = Fk + fk1 by A60;
then Fk1 . pq = 0 + (fk1 . pq) by A134, A135, A150, NAGATA_1:def_7, NAT_1:13;
hence (F . (k + 1)) . pq = 0 by A138, A142, A140, ABSVALUE:2; ::_thesis: verum
end;
end;
end;
A151: S10[ 0 ] ;
for n being Element of NAT holds S10[n] from NAT_1:sch_1(A151, A133);
hence (ADD "**" f) . pq = 0 by A129, A132; ::_thesis: verum
end;
end;
end;
hence (ADD "**" f) . [p,q] = 0 ; ::_thesis: verum
end;
A152: H4(H3(p1) \/ H3(q1)) is finite by A46;
then consider No being FinSequence such that
A153: rng No = H4(H5(p1,q1)) and
A154: No is one-to-one by A122, FINSEQ_4:58;
H4(H3(p1) \/ H3(q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A46;
then A155: H4(H5(p1,q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A122, XBOOLE_1:1;
then reconsider No = No as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A153, FINSEQ_1:def_4;
consider p2, q2 being Point of T such that
A156: [p2,q2] = pq2 and
A157: rng S2 = H4(H3(p2) \/ H3(q2)) by A57;
reconsider S1 = SFdist . pq1, S2 = SFdist . pq2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
set RNiS2 = H4(H5(p1,q1)) /\ H4(H3(p2) \/ H3(q2));
A158: S2 is one-to-one by A57;
A159: ( ADD is having_a_unity & ADD is commutative & ADD is associative ) by A60, NAGATA_1:23;
S1 is one-to-one by A57;
then consider S1No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S1No is one-to-one and
A160: rng S1No = (rng S1) \ (rng No) and
A161: ADD "**" S1 = ADD . ((ADD "**" No),(ADD "**" S1No)) by A114, A122, A153, A154, A159, Th18;
consider NoiS2 being FinSequence such that
A162: rng NoiS2 = H4(H5(p1,q1)) /\ H4(H3(p2) \/ H3(q2)) and
A163: NoiS2 is one-to-one by A122, A152, FINSEQ_4:58;
H4(H5(p1,q1)) /\ H4(H3(p2) \/ H3(q2)) c= H4(H5(p1,q1)) by XBOOLE_1:17;
then H4(H5(p1,q1)) /\ H4(H3(p2) \/ H3(q2)) c= Funcs ( the carrier of [:T,T:],REAL) by A155, XBOOLE_1:1;
then reconsider NoiS2 = NoiS2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A162, FINSEQ_1:def_4;
rng NoiS2 c= rng No by A153, A162, XBOOLE_1:17;
then consider NoNoiS2 being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
NoNoiS2 is one-to-one and
A164: rng NoNoiS2 = (rng No) \ (rng NoiS2) and
A165: ADD "**" No = ADD . ((ADD "**" NoiS2),(ADD "**" NoNoiS2)) by A154, A159, A163, Th18;
rng NoiS2 c= rng S2 by A157, A162, XBOOLE_1:17;
then consider S2No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S2No is one-to-one and
A166: rng S2No = (rng S2) \ (rng NoiS2) and
A167: ADD "**" S2 = ADD . ((ADD "**" NoiS2),(ADD "**" S2No)) by A159, A163, A158, Th18;
reconsider ANoNoiS2 = ADD "**" NoNoiS2, ANo = ADD "**" No, AS1No = ADD "**" S1No, AS2No = ADD "**" S2No, ANoiS2 = ADD "**" NoiS2, AS1 = ADD "**" S1, AS2 = ADD "**" S2 as RealMap of [:T,T:] by FUNCT_2:66;
rng S2No = H4(H3(p2) \/ H3(q2)) \ H4(H5(p1,q1)) by A157, A162, A166, XBOOLE_1:47;
then A168: AS2No . pq1 = 0 by A124, A113;
ANo = ANoiS2 + ANoNoiS2 by A60, A165;
then A169: ANo . pq1 = (ANoiS2 . pq1) + (ANoNoiS2 . pq1) by NAGATA_1:def_7;
AS1 = ANo + AS1No by A60, A161;
then A170: AS1 . pq1 = (ANo . pq1) + (AS1No . pq1) by NAGATA_1:def_7;
AS2 = ANoiS2 + AS2No by A60, A167;
then A171: AS2 . pq1 = (ANoiS2 . pq1) + (AS2No . pq1) by NAGATA_1:def_7;
A172: AS1No . pq1 = 0 by A124, A113, A114, A153, A160;
thus ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) ::_thesis: for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1
proof
A173: ADD is having_a_unity by A60, NAGATA_1:23;
then A174: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def_2;
assume A175: pq1 in SS . pq2 ; ::_thesis: (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1
now__::_thesis:_for_FD_being_set_st_FD_in_H4(H5(p1,q1))_holds_
FD_in_H4(H3(p2)_\/_H3(q2))
let FD be set ; ::_thesis: ( FD in H4(H5(p1,q1)) implies FD in H4(H3(p2) \/ H3(q2)) )
assume FD in H4(H5(p1,q1)) ; ::_thesis: FD in H4(H3(p2) \/ H3(q2))
then A176: ex fd being RealMap of T st
( FD = Fdist . fd & fd in H5(p1,q1) ) ;
H5(p1,q1) c= H3(p2) \/ H3(q2) by A115, A113, A156, A175;
hence FD in H4(H3(p2) \/ H3(q2)) by A176; ::_thesis: verum
end;
then H4(H5(p1,q1)) c= H4(H3(p2) \/ H3(q2)) by TARSKI:def_3;
then H4(H5(p1,q1)) /\ H4(H3(p2) \/ H3(q2)) = H4(H5(p1,q1)) by XBOOLE_1:28;
then rng NoNoiS2 = {} by A153, A162, A164, XBOOLE_1:37;
then NoNoiS2 = {} by RELAT_1:41;
then len NoNoiS2 = 0 ;
then ADD "**" NoNoiS2 = the_unity_wrt ADD by A173, FINSOP_1:def_1;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by A174, BINOP_1:def_8;
then A177: AS1 . pq1 = AS2 . pq1 by A111, A170, A169, A171, A172, A168;
SumFdist . pq1 = AS1 by A59;
hence (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 by A59, A177; ::_thesis: verum
end;
A178: ANoNoiS2 . (p1,q1) >= 0
proof
set N = NoNoiS2;
percases ( len NoNoiS2 = 0 or len NoNoiS2 <> 0 ) ;
supposeA179: len NoNoiS2 = 0 ; ::_thesis: ANoNoiS2 . (p1,q1) >= 0
A180: ADD is having_a_unity by A60, NAGATA_1:23;
then A181: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def_2;
ADD "**" NoNoiS2 = the_unity_wrt ADD by A179, A180, FINSOP_1:def_1;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by A181, BINOP_1:def_8;
hence ANoNoiS2 . (p1,q1) >= 0 by A111, A113; ::_thesis: verum
end;
supposeA182: len NoNoiS2 <> 0 ; ::_thesis: ANoNoiS2 . (p1,q1) >= 0
then len NoNoiS2 >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A183: F . 1 = NoNoiS2 . 1 and
A184: for n being Element of NAT st 0 <> n & n < len NoNoiS2 holds
F . (n + 1) = ADD . ((F . n),(NoNoiS2 . (n + 1))) and
A185: ADD "**" NoNoiS2 = F . (len NoNoiS2) by FINSOP_1:def_1;
defpred S10[ Element of NAT ] means ( $1 <> 0 & $1 <= len NoNoiS2 implies for Fn being RealMap of [:T,T:] st Fn = F . $1 holds
Fn . (p1,q1) >= 0 );
A186: for k being Element of NAT st S10[k] holds
S10[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S10[k] implies S10[k + 1] )
assume A187: S10[k] ; ::_thesis: S10[k + 1]
assume that
k + 1 <> 0 and
A188: k + 1 <= len NoNoiS2 ; ::_thesis: for Fn being RealMap of [:T,T:] st Fn = F . (k + 1) holds
Fn . (p1,q1) >= 0
A189: k < len NoNoiS2 by A188, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom NoNoiS2 by A188, FINSEQ_3:25;
then NoNoiS2 . (k + 1) in (rng No) \ (rng NoiS2) by A164, FUNCT_1:def_3;
then NoNoiS2 . (k + 1) in H4(H5(p1,q1)) by A153, XBOOLE_0:def_5;
then consider fd being RealMap of T such that
A190: Fdist . fd = NoNoiS2 . (k + 1) and
fd in H5(p1,q1) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, Nk1 = NoNoiS2 . (k + 1) as RealMap of [:T,T:] by A190, FUNCT_2:5, FUNCT_2:66;
A191: abs ((fd . p1) - (fd . q1)) >= 0 by COMPLEX1:46;
A192: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A193: Fdistfd . (p1,q1) = abs ((fd . p1) - (fd . q1)) by A42;
A194: now__::_thesis:_Fk1_._(p1,q1)_>=_0
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: Fk1 . (p1,q1) >= 0
hence Fk1 . (p1,q1) >= 0 by A42, A183, A190, A192, A191; ::_thesis: verum
end;
supposeA195: k > 0 ; ::_thesis: Fk1 . (p1,q1) >= 0
then Fk1 = ADD . (Fk,Nk1) by A184, A189;
then A196: Fk1 = Fk + Nk1 by A60;
Fk . (p1,q1) >= 0 by A187, A188, A195, NAT_1:13;
then 0 + 0 <= (Fk . (p1,q1)) + (Nk1 . (p1,q1)) by A190, A191, A193;
hence Fk1 . (p1,q1) >= 0 by A113, A196, NAGATA_1:def_7; ::_thesis: verum
end;
end;
end;
let Fn be RealMap of [:T,T:]; ::_thesis: ( Fn = F . (k + 1) implies Fn . (p1,q1) >= 0 )
assume Fn = F . (k + 1) ; ::_thesis: Fn . (p1,q1) >= 0
hence Fn . (p1,q1) >= 0 by A194; ::_thesis: verum
end;
A197: S10[ 0 ] ;
for n being Element of NAT holds S10[n] from NAT_1:sch_1(A197, A186);
hence ANoNoiS2 . (p1,q1) >= 0 by A182, A185; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_SumFdist1,_SumFdist2_being_RealMap_of_[:T,T:]_st_SumFdist1_=_SumFdist_._pq1_&_SumFdist2_=_SumFdist_._pq2_holds_
SumFdist1_._pq1_>=_SumFdist2_._pq1
A198: AS2 . (p1,q1) <= AS1 . (p1,q1) by A113, A178, A170, A169, A171, A172, A168, XREAL_1:7;
let SumFdist1, SumFdist2 be RealMap of [:T,T:]; ::_thesis: ( SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 implies SumFdist1 . pq1 >= SumFdist2 . pq1 )
assume that
A199: SumFdist1 = SumFdist . pq1 and
A200: SumFdist2 = SumFdist . pq2 ; ::_thesis: SumFdist1 . pq1 >= SumFdist2 . pq1
SumFdist2 = AS2 by A59, A200;
hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A59, A113, A199, A198; ::_thesis: verum
end;
hence for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Point_of_T_holds_
(_SumFTS_._(p,p)_=_0_&_SumFTS_._(p,r)_<=_(SumFTS_._(p,q))_+_(SumFTS_._(r,q))_)
let p, q, r be Point of T; ::_thesis: ( SumFTS . (p,p) = 0 & SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) )
thus SumFTS . (p,p) = 0 ::_thesis: SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q))
proof
reconsider pp = [p,p] as Point of [:T,T:] by BORSUK_1:def_2;
reconsider SF = SFdist . pp as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
A201: now__::_thesis:_(ADD_"**"_SF)_._pp_=_0
percases ( len SF = 0 or len SF <> 0 ) ;
supposeA202: len SF = 0 ; ::_thesis: (ADD "**" SF) . pp = 0
A203: ADD is having_a_unity by A60, NAGATA_1:23;
then A204: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def_2;
ADD "**" SF = the_unity_wrt ADD by A202, A203, FINSOP_1:def_1;
then ADD "**" SF is_a_unity_wrt ADD by A204, BINOP_1:def_8;
hence (ADD "**" SF) . pp = 0 by A111; ::_thesis: verum
end;
supposeA205: len SF <> 0 ; ::_thesis: (ADD "**" SF) . pp = 0
then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A206: F . 1 = SF . 1 and
A207: for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A208: ADD "**" SF = F . (len SF) by FINSOP_1:def_1;
defpred S10[ Element of NAT ] means ( $1 <> 0 & $1 <= len SF implies (F . $1) . pp = 0 );
A209: for k being Element of NAT st S10[k] holds
S10[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S10[k] implies S10[k + 1] )
assume A210: S10[k] ; ::_thesis: S10[k + 1]
consider x, y being Point of T such that
[x,y] = pp and
A211: rng SF = H4(H3(x) \/ H3(y)) by A57;
assume that
k + 1 <> 0 and
A212: k + 1 <= len SF ; ::_thesis: (F . (k + 1)) . pp = 0
A213: k < len SF by A212, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SF by A212, FINSEQ_3:25;
then SF . (k + 1) in H4(H3(x) \/ H3(y)) by A211, FUNCT_1:def_3;
then consider fd being RealMap of T such that
A214: Fdist . fd = SF . (k + 1) and
fd in H3(x) \/ H3(y) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SF . (k + 1) as RealMap of [:T,T:] by A214, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A215: Fdistfd . (p,p) = abs ((fd . p) - (fd . p)) by A42;
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: (F . (k + 1)) . pp = 0
hence (F . (k + 1)) . pp = 0 by A206, A214, A215, ABSVALUE:2; ::_thesis: verum
end;
supposeA216: k > 0 ; ::_thesis: (F . (k + 1)) . pp = 0
then Fk1 = ADD . (Fk,SFk1) by A207, A213;
then Fk1 = Fk + SFk1 by A60;
then Fk1 . pp = 0 + (SFk1 . pp) by A210, A212, A216, NAGATA_1:def_7, NAT_1:13;
hence (F . (k + 1)) . pp = 0 by A214, A215, ABSVALUE:2; ::_thesis: verum
end;
end;
end;
A217: S10[ 0 ] ;
for n being Element of NAT holds S10[n] from NAT_1:sch_1(A217, A209);
hence (ADD "**" SF) . pp = 0 by A205, A208; ::_thesis: verum
end;
end;
end;
SumFdist . pp = ADD "**" SF by A59;
hence SumFTS . (p,p) = 0 by A201, NAGATA_1:def_8; ::_thesis: verum
end;
thus SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) ::_thesis: verum
proof
reconsider pr = [p,r], pq = [p,q], rq = [r,q] as Point of [:T,T:] by BORSUK_1:def_2;
reconsider SFpr = SFdist . pr as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
reconsider ASFpr = ADD "**" SFpr as RealMap of [:T,T:] by FUNCT_2:66;
reconsider SumFpr = SumFdist . pr, SumFpq = SumFdist . pq, SumFrq = SumFdist . rq as RealMap of [:T,T:] by FUNCT_2:66;
A218: ( SumFTS . pr = SumFpr . pr & SumFTS . pq = SumFpq . pq ) by NAGATA_1:def_8;
( SumFpr . pq <= SumFpq . pq & SumFpr . rq <= SumFrq . rq ) by A112;
then A219: (SumFpr . pq) + (SumFpr . rq) <= (SumFpq . pq) + (SumFrq . rq) by XREAL_1:7;
A220: now__::_thesis:_ASFpr_._pr_<=_(ASFpr_._pq)_+_(ASFpr_._rq)
percases ( len SFpr = 0 or len SFpr <> 0 ) ;
supposeA221: len SFpr = 0 ; ::_thesis: ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq)
A222: ADD is having_a_unity by A60, NAGATA_1:23;
then A223: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def_2;
ADD "**" SFpr = the_unity_wrt ADD by A221, A222, FINSOP_1:def_1;
then A224: ADD "**" SFpr is_a_unity_wrt ADD by A223, BINOP_1:def_8;
then ( ASFpr . pr = 0 & ASFpr . pq = 0 ) by A111;
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A111, A224; ::_thesis: verum
end;
supposeA225: len SFpr <> 0 ; ::_thesis: ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq)
then len SFpr >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A226: F . 1 = SFpr . 1 and
A227: for n being Element of NAT st 0 <> n & n < len SFpr holds
F . (n + 1) = ADD . ((F . n),(SFpr . (n + 1))) and
A228: ADD "**" SFpr = F . (len SFpr) by FINSOP_1:def_1;
defpred S10[ Element of NAT ] means ( $1 <> 0 & $1 <= len SFpr implies for F9 being RealMap of [:T,T:] st F9 = F . $1 holds
F9 . pr <= (F9 . pq) + (F9 . rq) );
A229: for k being Element of NAT st S10[k] holds
S10[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S10[k] implies S10[k + 1] )
assume A230: S10[k] ; ::_thesis: S10[k + 1]
consider x, y being Point of T such that
[x,y] = pr and
A231: rng SFpr = H4(H3(x) \/ H3(y)) by A57;
assume that
k + 1 <> 0 and
A232: k + 1 <= len SFpr ; ::_thesis: for F9 being RealMap of [:T,T:] st F9 = F . (k + 1) holds
F9 . pr <= (F9 . pq) + (F9 . rq)
A233: k < len SFpr by A232, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SFpr by A232, FINSEQ_3:25;
then SFpr . (k + 1) in H4(H3(x) \/ H3(y)) by A231, FUNCT_1:def_3;
then consider fd being RealMap of T such that
A234: Fdist . fd = SFpr . (k + 1) and
fd in H3(x) \/ H3(y) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SFpr . (k + 1) as RealMap of [:T,T:] by A234, FUNCT_2:5, FUNCT_2:66;
A235: (fd . p) - (fd . r) = ((fd . p) - (fd . q)) + ((fd . q) - (fd . r)) ;
then A236: abs ((fd . p) - (fd . r)) <= (abs ((fd . p) - (fd . q))) + (abs ((fd . q) - (fd . r))) by COMPLEX1:56;
A237: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A238: ( Fdistfd . (p,r) = abs ((fd . p) - (fd . r)) & Fdistfd . (p,q) = abs ((fd . p) - (fd . q)) ) by A42;
A239: ( abs ((fd . q) - (fd . r)) = abs (- ((fd . q) - (fd . r))) & Fdistfd . (r,q) = abs ((fd . r) - (fd . q)) ) by A42, A237, COMPLEX1:52;
let F9 be RealMap of [:T,T:]; ::_thesis: ( F9 = F . (k + 1) implies F9 . pr <= (F9 . pq) + (F9 . rq) )
assume A240: F9 = F . (k + 1) ; ::_thesis: F9 . pr <= (F9 . pq) + (F9 . rq)
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: F9 . pr <= (F9 . pq) + (F9 . rq)
hence F9 . pr <= (F9 . pq) + (F9 . rq) by A226, A234, A235, A238, A239, A240, COMPLEX1:56; ::_thesis: verum
end;
supposeA241: k > 0 ; ::_thesis: F9 . pr <= (F9 . pq) + (F9 . rq)
then Fk . pr <= (Fk . pq) + (Fk . rq) by A230, A232, NAT_1:13;
then A242: (Fk . pr) + (SFk1 . pr) <= ((Fk . pq) + (Fk . rq)) + ((SFk1 . pq) + (SFk1 . rq)) by A234, A236, A238, A239, XREAL_1:7;
Fk1 = ADD . (Fk,SFk1) by A227, A233, A241;
then A243: Fk1 = Fk + SFk1 by A60;
then ( Fk1 . pq = (Fk . pq) + (SFk1 . pq) & Fk1 . rq = (Fk . rq) + (SFk1 . rq) ) by NAGATA_1:def_7;
hence F9 . pr <= (F9 . pq) + (F9 . rq) by A240, A243, A242, NAGATA_1:def_7; ::_thesis: verum
end;
end;
end;
A244: S10[ 0 ] ;
for n being Element of NAT holds S10[n] from NAT_1:sch_1(A244, A229);
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A225, A228; ::_thesis: verum
end;
end;
end;
SumFpr = ADD "**" SFpr by A59;
then SumFpr . pr <= (SumFpq . pq) + (SumFrq . rq) by A220, A219, XXREAL_0:2;
hence SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) by A218, NAGATA_1:def_8; ::_thesis: verum
end;
end;
then A245: SumFTS is_a_pseudometric_of the carrier of T by NAGATA_1:28;
A246: for p being Point of T
for fd being Element of Funcs ( the carrier of T,REAL) st fd in H3(p) holds
( S4[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
proof
let p be Point of T; ::_thesis: for fd being Element of Funcs ( the carrier of T,REAL) st fd in H3(p) holds
( S4[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
let fd be Element of Funcs ( the carrier of T,REAL); ::_thesis: ( fd in H3(p) implies ( S4[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) )
reconsider FD = Fdist . fd as RealMap of [:T,T:] by FUNCT_2:66;
assume fd in H3(p) ; ::_thesis: ( S4[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
then consider A being Subset of T such that
A247: fd = Fn . A and
A248: A in Bn . n and
A in H2(Sx . p) ;
A249: S4[fd,Fdist . fd] by A42;
S6[A,Fn . A] by A24, A248;
then FD is continuous by A247, A249, NAGATA_1:21;
hence ( S4[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) by A42; ::_thesis: verum
end;
A250: for pq9 being Point of [:T,T:] holds SumFdist . pq9 is continuous RealMap of [:T,T:]
proof
let pq9 be Point of [:T,T:]; ::_thesis: SumFdist . pq9 is continuous RealMap of [:T,T:]
reconsider SF = SFdist . pq9 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def_11;
consider p, q being Point of T such that
[p,q] = pq9 and
A251: rng SF = H4(H3(p) \/ H3(q)) by A57;
for n being Element of NAT st 0 <> n & n <= len SF holds
SF . n is continuous RealMap of [:T,T:]
proof
let n be Element of NAT ; ::_thesis: ( 0 <> n & n <= len SF implies SF . n is continuous RealMap of [:T,T:] )
assume that
A252: 0 <> n and
A253: n <= len SF ; ::_thesis: SF . n is continuous RealMap of [:T,T:]
n >= 1 by A252, NAT_1:14;
then n in dom SF by A253, FINSEQ_3:25;
then SF . n in H4(H3(p) \/ H3(q)) by A251, FUNCT_1:def_3;
then consider fd being RealMap of T such that
A254: SF . n = Fdist . fd and
A255: fd in H3(p) \/ H3(q) ;
A256: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
( fd in H3(p) or fd in H3(q) ) by A255, XBOOLE_0:def_3;
hence SF . n is continuous RealMap of [:T,T:] by A246, A254, A256; ::_thesis: verum
end;
then ADD "**" SF is continuous RealMap of [:T,T:] by A60, NAGATA_1:25;
hence SumFdist . pq9 is continuous RealMap of [:T,T:] by A59; ::_thesis: verum
end;
A257: for pq9 being Point of [:T,T:] holds SumFdist9 . pq9 is continuous Function of [:T,T:],R^1
proof
let pq9 be Point of [:T,T:]; ::_thesis: SumFdist9 . pq9 is continuous Function of [:T,T:],R^1
reconsider SF = SumFdist . pq9 as Function of [:T,T:],R^1 by A250, TOPMETR:17;
SumFdist . pq9 is continuous RealMap of [:T,T:] by A250;
then SF is continuous by JORDAN5A:27;
hence SumFdist9 . pq9 is continuous Function of [:T,T:],R^1 ; ::_thesis: verum
end;
take min (1,SumFTS9) ; ::_thesis: S1[n,m, min (1,SumFTS9)]
A258: for p, q being Point of T holds (min (1,SumFTS9)) . [p,q] <= 1
proof
let p, q be Point of T; ::_thesis: (min (1,SumFTS9)) . [p,q] <= 1
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then (min (1,SumFTS9)) . [p,q] = min (1,(SumFTS9 . [p,q])) by NAGATA_1:def_9;
hence (min (1,SumFTS9)) . [p,q] <= 1 by XXREAL_0:17; ::_thesis: verum
end;
for p, q being Point of [:T,T:] st p in SS . q holds
(SumFdist9 . p) . p = (SumFdist9 . q) . p by A112;
then SumFdist9 Toler is continuous by A257, A32, NAGATA_1:26;
then SumFTS9 is continuous by JORDAN5A:27;
then ( min (1,SumFTS9) = min (1,SumFTS) & min (1,SumFTS9) is continuous ) by BORSUK_1:def_2, NAGATA_1:27;
hence S1[n,m, min (1,SumFTS9)] by A245, A258, A109, NAGATA_1:30; ::_thesis: verum
end;
A259: for k being set st k in NAT holds
ex f being set st
( f in Funcs ( the carrier of [:T,T:],REAL) & S2[k,f] )
proof
A260: NAT = rng PairFunc by Th2, FUNCT_2:def_3;
let k be set ; ::_thesis: ( k in NAT implies ex f being set st
( f in Funcs ( the carrier of [:T,T:],REAL) & S2[k,f] ) )
assume k in NAT ; ::_thesis: ex f being set st
( f in Funcs ( the carrier of [:T,T:],REAL) & S2[k,f] )
then consider nm being set such that
A261: nm in dom PairFunc and
A262: k = PairFunc . nm by A260, FUNCT_1:def_3;
consider n, m being set such that
A263: ( n in NAT & m in NAT ) and
A264: nm = [n,m] by A261, ZFMISC_1:def_2;
consider pmet9 being RealMap of [:T,T:] such that
A265: S1[n,m,pmet9] by A7, A263;
take pmet9 ; ::_thesis: ( pmet9 in Funcs ( the carrier of [:T,T:],REAL) & S2[k,pmet9] )
thus pmet9 in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8; ::_thesis: S2[k,pmet9]
take pm = pmet9; ::_thesis: ( pm = pmet9 & ( for n, m being Element of NAT st (PairFunc ") . k = [n,m] holds
S1[n,m,pm] ) )
thus pm = pmet9 ; ::_thesis: for n, m being Element of NAT st (PairFunc ") . k = [n,m] holds
S1[n,m,pm]
let n1, m1 be Element of NAT ; ::_thesis: ( (PairFunc ") . k = [n1,m1] implies S1[n1,m1,pm] )
assume (PairFunc ") . k = [n1,m1] ; ::_thesis: S1[n1,m1,pm]
then [n1,m1] = [n,m] by A261, A262, A264, Lm2, Th2, FUNCT_1:32;
then ( n1 = n & m1 = m ) by XTUPLE_0:1;
hence S1[n1,m1,pm] by A265; ::_thesis: verum
end;
consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A266: for n being set st n in NAT holds
S2[n,F . n] from FUNCT_2:sch_1(A259);
A267: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_PartFunc_of_[:_the_carrier_of_T,_the_carrier_of_T:],REAL
let n be Element of NAT ; ::_thesis: F . n is PartFunc of [: the carrier of T, the carrier of T:],REAL
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def_2;
hence F . n is PartFunc of [: the carrier of T, the carrier of T:],REAL by FUNCT_2:66; ::_thesis: verum
end;
dom F = NAT by FUNCT_2:def_1;
then reconsider F9 = F as Functional_Sequence of [: the carrier of T, the carrier of T:],REAL by A267, SEQFUNC:1;
A268: for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex k being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . k = pmet holds
(lower_bound (pmet,A9)) . p > 0
proof
let p be Point of T; ::_thesis: for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex k being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . k = pmet holds
(lower_bound (pmet,A9)) . p > 0
let A9 be non empty Subset of T; ::_thesis: ( not p in A9 & A9 is closed implies ex k being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . k = pmet holds
(lower_bound (pmet,A9)) . p > 0 )
assume that
A269: not p in A9 and
A270: A9 is closed ; ::_thesis: ex k being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . k = pmet holds
(lower_bound (pmet,A9)) . p > 0
set O = A9 ` ;
p in A9 ` by A269, XBOOLE_0:def_5;
then consider U being Subset of T such that
A271: p in U and
A272: Cl U c= A9 ` and
A273: U in Union Bn by A1, A5, A270, NAGATA_1:19;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider U = U as open Subset of T by A273, PRE_TOPC:def_2;
consider n being Element of NAT such that
A274: U in Bn . n by A273, PROB_1:12;
consider W being Subset of T such that
A275: ( p in W & Cl W c= U ) and
A276: W in Union Bn by A1, A5, A271, NAGATA_1:19;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider W = W as open Subset of T by A276, PRE_TOPC:def_2;
consider m being Element of NAT such that
A277: W in Bn . m by A276, PROB_1:12;
set k = PairFunc . [n,m];
consider G being RealMap of [:T,T:] such that
A278: G = F . (PairFunc . [n,m]) and
A279: for n, m being Element of NAT st (PairFunc ") . (PairFunc . [n,m]) = [n,m] holds
S1[n,m,G] by A266;
dom PairFunc = [:NAT,NAT:] by FUNCT_2:def_1;
then [n,m] = (PairFunc ") . (PairFunc . [n,m]) by Lm2, Th2, FUNCT_1:32;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A280: G = pmet and
G is continuous and
pmet is_a_pseudometric_of the carrier of T and
A281: for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) by A279;
A282: for rn being real number st rn in (dist (pmet,p)) .: A9 holds
rn >= 1
proof
let rn be real number ; ::_thesis: ( rn in (dist (pmet,p)) .: A9 implies rn >= 1 )
assume rn in (dist (pmet,p)) .: A9 ; ::_thesis: rn >= 1
then consider a being set such that
A283: a in dom (dist (pmet,p)) and
A284: a in A9 and
A285: rn = (dist (pmet,p)) . a by FUNCT_1:def_6;
reconsider a = a as Point of T by A283;
A286: pmet . (p,a) = (dist (pmet,p)) . a by Def2;
U c= Cl U by PRE_TOPC:18;
then U c= A9 ` by A272, XBOOLE_1:1;
then U misses A9 by SUBSET_1:23;
then not a in U by A284, XBOOLE_0:3;
hence rn >= 1 by A275, A274, A277, A281, A285, A286; ::_thesis: verum
end;
take PairFunc . [n,m] ; ::_thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . (PairFunc . [n,m]) = pmet holds
(lower_bound (pmet,A9)) . p > 0
the carrier of T = dom (dist (pmet,p)) by FUNCT_2:def_1;
then lower_bound ((dist (pmet,p)) .: A9) >= 1 by A282, SEQ_4:43;
hence for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . (PairFunc . [n,m]) = pmet holds
(lower_bound (pmet,A9)) . p > 0 by A278, A280, Def3; ::_thesis: verum
end;
for k being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
proof
let k be Element of NAT ; ::_thesis: ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
consider Fk being RealMap of [:T,T:] such that
A287: Fk = F . k and
A288: for n, m being Element of NAT st (PairFunc ") . k = [n,m] holds
S1[n,m,Fk] by A266;
NAT = rng PairFunc by Th2, FUNCT_2:def_3;
then consider nm being set such that
A289: nm in dom PairFunc and
A290: k = PairFunc . nm by FUNCT_1:def_3;
consider n, m being set such that
A291: ( n in NAT & m in NAT ) and
A292: nm = [n,m] by A289, ZFMISC_1:def_2;
[n,m] = (PairFunc ") . k by A289, A290, A292, Lm2, Th2, FUNCT_1:32;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A293: Fk = pmet and
A294: Fk is continuous and
A295: pmet is_a_pseudometric_of the carrier of T and
A296: for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) by A291, A288;
take pmet ; ::_thesis: ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
thus ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A287, A293, A295; ::_thesis: ( ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
thus for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 ::_thesis: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous
proof
let pq be Element of [: the carrier of T, the carrier of T:]; ::_thesis: pmet . pq <= 1
ex p, q being set st
( p in the carrier of T & q in the carrier of T & pq = [p,q] ) by ZFMISC_1:def_2;
hence pmet . pq <= 1 by A296; ::_thesis: verum
end;
thus for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous by A293, A294; ::_thesis: verum
end;
hence T is metrizable by A2, A268, Th17; ::_thesis: verum
end;
thus ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) ) by NAGATA_1:15, NAGATA_1:16; ::_thesis: verum
end;
theorem Th20: :: NAGATA_2:20
for T being non empty TopSpace st T is metrizable holds
for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
proof
let T be non empty TopSpace; ::_thesis: ( T is metrizable implies for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete ) )
set cT = the carrier of T;
assume T is metrizable ; ::_thesis: for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that
A1: metr is_metric_of the carrier of T and
A2: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by PCOMPS_1:def_8;
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A1, PCOMPS_1:36;
set cPM = the carrier of PM;
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of T & FX is open implies ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete ) )
assume that
A3: FX is Cover of T and
A4: FX is open ; ::_thesis: ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
defpred S1[ set ] means $1 in FX;
deffunc H1( Point of PM, Nat) -> Element of bool the carrier of PM = Ball ($1,(1 / (2 |^ ($2 + 1))));
consider R being Relation such that
A5: R well_orders FX by WELLORD2:17;
consider Mn being Relation such that
A6: Mn = R |_2 FX ;
set UB = { (union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ) where V is Subset of PM : V in FX } ;
{ (union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ) where V is Subset of PM : V in FX } c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ) where V is Subset of PM : V in FX } or x in bool the carrier of PM )
assume x in { (union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ) where V is Subset of PM : V in FX } ; ::_thesis: x in bool the carrier of PM
then consider V being Subset of PM such that
A7: x = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } and
V in FX ;
x c= the carrier of PM
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in the carrier of PM )
assume y in x ; ::_thesis: y in the carrier of PM
then consider W being set such that
A8: y in W and
A9: W in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } by A7, TARSKI:def_4;
ex c being Point of PM st
( W = Ball (c,(1 / 2)) & c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) by A9;
hence y in the carrier of PM by A8; ::_thesis: verum
end;
hence x in bool the carrier of PM ; ::_thesis: verum
end;
then reconsider UB = { (union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ) where V is Subset of PM : V in FX } as Subset-Family of PM ;
defpred S2[ Point of PM, Subset of PM, Nat] means ( $1 in $2 \ (PartUnion ($2,Mn)) & Ball ($1,(3 / (2 |^ ($3 + 1)))) c= $2 );
consider Un being Function of NAT,(bool (bool the carrier of PM)) such that
A10: ( Un . 0 = UB & ( for n being Element of NAT holds Un . (n + 1) = { (union { H1(c,n) where c is Point of PM : ( S2[c,V,n] & not c in union { (union (Un . k)) where k is Element of NAT : k <= n } ) } ) where V is Subset of PM : S1[V] } ) ) from PCOMPS_2:sch_3();
reconsider Un9 = Un as FamilySequence of T by A1, PCOMPS_2:4;
take Un9 ; ::_thesis: ( Union Un9 is open & Union Un9 is Cover of T & Union Un9 is_finer_than FX & Un9 is sigma_discrete )
thus Union Un9 is open ::_thesis: ( Union Un9 is Cover of T & Union Un9 is_finer_than FX & Un9 is sigma_discrete )
proof
let A be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not A in Union Un9 or A is open )
assume A in Union Un9 ; ::_thesis: A is open
then consider n being Element of NAT such that
A11: A in Un . n by PROB_1:12;
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: A is open
then consider V being Subset of PM such that
A12: A = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } and
V in FX by A10, A11;
set BALL = { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ;
{ (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } or x in bool the carrier of PM )
assume x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ; ::_thesis: x in bool the carrier of PM
then ex c being Point of PM st
( x = Ball (c,(1 / 2)) & c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) ;
hence x in bool the carrier of PM ; ::_thesis: verum
end;
then reconsider BALL = { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } as Subset-Family of PM ;
BALL c= Family_open_set PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BALL or x in Family_open_set PM )
assume x in BALL ; ::_thesis: x in Family_open_set PM
then ex c being Point of PM st
( x = Ball (c,(1 / 2)) & c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) ;
hence x in Family_open_set PM by PCOMPS_1:29; ::_thesis: verum
end;
then A in the topology of T by A2, A12, PCOMPS_1:32;
hence A is open by PRE_TOPC:def_2; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: A is open
then consider m being Nat such that
A13: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A in { (union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S1[V] } by A10, A11, A13;
then consider V being Subset of PM such that
A14: ( A = union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S1[V] ) ;
set BALL = { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ;
{ H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } or x in bool the carrier of PM )
assume x in { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ; ::_thesis: x in bool the carrier of PM
then ex c being Point of PM st
( x = H1(c,m) & S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
hence x in bool the carrier of PM ; ::_thesis: verum
end;
then reconsider BALL = { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } as Subset-Family of PM ;
BALL c= Family_open_set PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BALL or x in Family_open_set PM )
assume x in BALL ; ::_thesis: x in Family_open_set PM
then ex c being Point of PM st
( x = H1(c,m) & S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
hence x in Family_open_set PM by PCOMPS_1:29; ::_thesis: verum
end;
then A in the topology of T by A2, A14, PCOMPS_1:32;
hence A is open by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
A15: Mn well_orders FX by A5, A6, PCOMPS_2:1;
[#] T c= union (Union Un9)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union (Union Un9) )
assume A16: x in [#] T ; ::_thesis: x in union (Union Un9)
reconsider x9 = x as Element of PM by A1, A16, PCOMPS_2:4;
defpred S3[ set ] means x in $1;
ex G being Subset of T st
( x in G & G in FX ) by A3, A16, PCOMPS_1:3;
then A17: ex G being set st
( G in FX & S3[G] ) ;
consider X being set such that
A18: ( X in FX & S3[X] & ( for Y being set st Y in FX & S3[Y] holds
[X,Y] in Mn ) ) from PCOMPS_2:sch_1(A15, A17);
assume A19: not x in union (Union Un9) ; ::_thesis: contradiction
A20: for V being set
for n being Element of NAT st V in Un9 . n holds
not x in V
proof
let V be set ; ::_thesis: for n being Element of NAT st V in Un9 . n holds
not x in V
let n be Element of NAT ; ::_thesis: ( V in Un9 . n implies not x in V )
assume V in Un9 . n ; ::_thesis: not x in V
then V in Union Un by PROB_1:12;
hence not x in V by A19, TARSKI:def_4; ::_thesis: verum
end;
A21: for n being Element of NAT holds not x in union (Un9 . n)
proof
let n be Element of NAT ; ::_thesis: not x in union (Un9 . n)
assume x in union (Un9 . n) ; ::_thesis: contradiction
then ex V being set st
( x in V & V in Un9 . n ) by TARSKI:def_4;
hence contradiction by A20; ::_thesis: verum
end;
reconsider X = X as Subset of T by A18;
X is open by A4, A18, TOPS_2:def_1;
then A22: X in Family_open_set PM by A2, PRE_TOPC:def_2;
reconsider X = X as Subset of PM by A1, PCOMPS_2:4;
consider r being Real such that
A23: r > 0 and
A24: Ball (x9,r) c= X by A18, A22, PCOMPS_1:def_4;
defpred S4[ Nat] means 3 / (2 |^ $1) <= r;
ex k being Element of NAT st S4[k] by A23, PREPOWER:92;
then A25: ex k being Nat st S4[k] ;
consider k being Nat such that
A26: ( S4[k] & ( for i being Nat st S4[i] holds
k <= i ) ) from NAT_1:sch_5(A25);
set W = union { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } ;
2 |^ (k + 1) = (2 |^ k) * 2 by NEWTON:6;
then ( 2 |^ k > 0 & 2 |^ (k + 1) >= 2 |^ k ) by PREPOWER:6, XREAL_1:151;
then 3 / (2 |^ (k + 1)) <= 3 / (2 |^ k) by XREAL_1:118;
then A27: 3 / (2 |^ (k + 1)) <= r by A26, XXREAL_0:2;
A28: x in union { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) }
proof
not x9 in PartUnion (X,Mn)
proof
assume x9 in PartUnion (X,Mn) ; ::_thesis: contradiction
then x9 in union (Mn -Seg X) by PCOMPS_2:def_1;
then consider M being set such that
A29: x9 in M and
A30: M in Mn -Seg X by TARSKI:def_4;
A31: M <> X by A30, WELLORD1:1;
A32: Mn is_antisymmetric_in FX by A15, WELLORD1:def_5;
A33: [M,X] in Mn by A30, WELLORD1:1;
then M in field Mn by RELAT_1:15;
then A34: M in FX by A5, A6, PCOMPS_2:1;
then [X,M] in Mn by A18, A29;
hence contradiction by A18, A31, A33, A34, A32, RELAT_2:def_4; ::_thesis: verum
end;
then A35: x9 in X \ (PartUnion (X,Mn)) by A18, XBOOLE_0:def_5;
set A = Ball (x9,(1 / (2 |^ (k + 1))));
0 < 2 |^ (k + 1) by PREPOWER:6;
then A36: x9 in Ball (x9,(1 / (2 |^ (k + 1)))) by TBSP_1:11, XREAL_1:139;
A37: not x9 in union { (union (Un9 . i)) where i is Element of NAT : i <= k }
proof
assume x9 in union { (union (Un9 . i)) where i is Element of NAT : i <= k } ; ::_thesis: contradiction
then consider D being set such that
A38: ( x9 in D & D in { (union (Un9 . i)) where i is Element of NAT : i <= k } ) by TARSKI:def_4;
ex i being Element of NAT st
( D = union (Un9 . i) & i <= k ) by A38;
hence contradiction by A21, A38; ::_thesis: verum
end;
Ball (x9,(3 / (2 |^ (k + 1)))) c= Ball (x9,r) by A27, PCOMPS_1:1;
then Ball (x9,(3 / (2 |^ (k + 1)))) c= X by A24, XBOOLE_1:1;
then Ball (x9,(1 / (2 |^ (k + 1)))) in { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un9 . i)) where i is Element of NAT : i <= k } ) } by A35, A37;
hence x in union { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } by A36, TARSKI:def_4; ::_thesis: verum
end;
( k in NAT & union { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } in { (union { H1(y,k) where y is Point of PM : ( S2[y,V,k] & not y in union { (union (Un . q)) where q is Element of NAT : q <= k } ) } ) where V is Subset of PM : V in FX } ) by A18, ORDINAL1:def_12;
then union { H1(y,k) where y is Point of PM : ( S2[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } in Un9 . (k + 1) by A10;
hence contradiction by A20, A28; ::_thesis: verum
end;
then [#] T = union (Union Un9) by XBOOLE_0:def_10;
hence Union Un9 is Cover of T by SETFAM_1:45; ::_thesis: ( Union Un9 is_finer_than FX & Un9 is sigma_discrete )
for X being set st X in Union Un9 holds
ex Y being set st
( Y in FX & X c= Y )
proof
let X be set ; ::_thesis: ( X in Union Un9 implies ex Y being set st
( Y in FX & X c= Y ) )
assume X in Union Un9 ; ::_thesis: ex Y being set st
( Y in FX & X c= Y )
then consider n being Element of NAT such that
A39: X in Un . n by PROB_1:12;
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: ex Y being set st
( Y in FX & X c= Y )
then consider V being Subset of PM such that
A40: X = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } and
A41: V in FX by A10, A39;
set BALL = { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ;
{ (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } or x in bool the carrier of PM )
assume x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } ; ::_thesis: x in bool the carrier of PM
then ex c being Point of PM st
( x = Ball (c,(1 / 2)) & c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) ;
hence x in bool the carrier of PM ; ::_thesis: verum
end;
then reconsider BALL = { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } as Subset-Family of PM ;
for W being set st W in BALL holds
W c= V
proof
let W be set ; ::_thesis: ( W in BALL implies W c= V )
assume W in BALL ; ::_thesis: W c= V
then consider c being Element of PM such that
A42: W = Ball (c,(1 / 2)) and
c in V \ (PartUnion (V,Mn)) and
A43: Ball (c,(3 / 2)) c= V ;
Ball (c,(1 / 2)) c= Ball (c,(3 / 2)) by PCOMPS_1:1;
hence W c= V by A42, A43, XBOOLE_1:1; ::_thesis: verum
end;
then X c= V by A40, ZFMISC_1:76;
hence ex Y being set st
( Y in FX & X c= Y ) by A41; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex Y being set st
( Y in FX & X c= Y )
then consider m being Nat such that
A44: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
X in { (union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S1[V] } by A10, A39, A44;
then consider V being Subset of PM such that
A45: ( X = union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S1[V] ) ;
set BALL = { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ;
{ H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } or x in bool the carrier of PM )
assume x in { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ; ::_thesis: x in bool the carrier of PM
then ex c being Point of PM st
( x = H1(c,m) & S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
hence x in bool the carrier of PM ; ::_thesis: verum
end;
then reconsider BALL = { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } as Subset-Family of PM ;
for W being set st W in BALL holds
W c= V
proof
let W be set ; ::_thesis: ( W in BALL implies W c= V )
assume W in BALL ; ::_thesis: W c= V
then consider c being Element of PM such that
A46: ( W = H1(c,m) & S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
0 < 2 |^ (m + 1) by PREPOWER:6;
then 1 / (2 |^ (m + 1)) < 3 / (2 |^ (m + 1)) by XREAL_1:74;
then H1(c,m) c= Ball (c,(3 / (2 |^ (m + 1)))) by PCOMPS_1:1;
hence W c= V by A46, XBOOLE_1:1; ::_thesis: verum
end;
then X c= V by A45, ZFMISC_1:76;
hence ex Y being set st
( Y in FX & X c= Y ) by A45; ::_thesis: verum
end;
end;
end;
hence Union Un9 is_finer_than FX by SETFAM_1:def_2; ::_thesis: Un9 is sigma_discrete
for n being Element of NAT holds Un9 . n is discrete
proof
let n be Element of NAT ; ::_thesis: Un9 . n is discrete
for p being Point of T ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )
proof
let p be Point of T; ::_thesis: ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )
reconsider p9 = p as Point of PM by A1, PCOMPS_2:4;
set O = Ball (p9,(1 / (2 |^ (n + 2))));
Ball (p9,(1 / (2 |^ (n + 2)))) in Family_open_set PM by PCOMPS_1:29;
then reconsider O = Ball (p9,(1 / (2 |^ (n + 2)))) as open Subset of T by A2, PRE_TOPC:def_2;
take O ; ::_thesis: ( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )
A47: now__::_thesis:_for_A,_B_being_Subset_of_T_st_A_in_Un9_._n_&_B_in_Un9_._n_&_O_meets_A_&_O_meets_B_holds_
A_=_B
let A, B be Subset of T; ::_thesis: ( A in Un9 . n & B in Un9 . n & O meets A & O meets B implies A = B )
assume that
A48: A in Un9 . n and
A49: B in Un9 . n ; ::_thesis: ( O meets A & O meets B implies A = B )
assume that
A50: O meets A and
A51: O meets B ; ::_thesis: A = B
consider a being set such that
A52: a in O and
A53: a in A by A50, XBOOLE_0:3;
consider b being set such that
A54: b in O and
A55: b in B by A51, XBOOLE_0:3;
reconsider a = a, b = b as Point of PM by A52, A54;
A56: dist (p9,b) < 1 / (2 |^ (n + 2)) by A54, METRIC_1:11;
A57: ( dist (a,b) <= (dist (a,p9)) + (dist (p9,b)) & 2 |^ ((n + 1) + 1) = (2 |^ (n + 1)) * 2 ) by METRIC_1:4, NEWTON:6;
dist (p9,a) < 1 / (2 |^ (n + 2)) by A52, METRIC_1:11;
then (dist (a,p9)) + (dist (p9,b)) < (1 / (2 |^ (n + 2))) + (1 / (2 |^ (n + 2))) by A56, XREAL_1:8;
then dist (a,b) < 2 * (1 / (2 * (2 |^ (n + 1)))) by A57, XXREAL_0:2;
then dist (a,b) < (2 * 1) / (2 * (2 |^ (n + 1))) by XCMPLX_1:74;
then A58: dist (a,b) < ((2 / 2) * 1) / (2 |^ (n + 1)) by XCMPLX_1:83;
now__::_thesis:_A_=_B
percases ( n = 0 or n > 0 ) ;
supposeA59: n = 0 ; ::_thesis: A = B
then A60: dist (a,b) < 1 / 2 by A58, NEWTON:5;
consider V being Subset of PM such that
A61: A = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } and
A62: V in FX by A10, A48, A59;
consider Ba being set such that
A63: a in Ba and
A64: Ba in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } by A53, A61, TARSKI:def_4;
consider ca being Point of PM such that
A65: Ba = Ball (ca,(1 / 2)) and
A66: ca in V \ (PartUnion (V,Mn)) and
A67: Ball (ca,(3 / 2)) c= V by A64;
dist (ca,a) < 1 / 2 by A63, A65, METRIC_1:11;
then A68: (dist (ca,a)) + (dist (a,b)) < (1 / 2) + (1 / 2) by A60, XREAL_1:8;
dist (ca,b) <= (dist (ca,a)) + (dist (a,b)) by METRIC_1:4;
then A69: dist (ca,b) < 1 by A68, XXREAL_0:2;
consider W being Subset of PM such that
A70: B = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in W \ (PartUnion (W,Mn)) & Ball (c,(3 / 2)) c= W ) } and
A71: W in FX by A10, A49, A59;
consider Bb being set such that
A72: b in Bb and
A73: Bb in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in W \ (PartUnion (W,Mn)) & Ball (c,(3 / 2)) c= W ) } by A55, A70, TARSKI:def_4;
consider cb being Point of PM such that
A74: Bb = Ball (cb,(1 / 2)) and
A75: cb in W \ (PartUnion (W,Mn)) and
A76: Ball (cb,(3 / 2)) c= W by A73;
A77: dist (ca,cb) <= (dist (ca,b)) + (dist (b,cb)) by METRIC_1:4;
dist (cb,b) < 1 / 2 by A72, A74, METRIC_1:11;
then (dist (ca,b)) + (dist (b,cb)) < 1 + (1 / 2) by A69, XREAL_1:8;
then dist (ca,cb) < 3 / 2 by A77, XXREAL_0:2;
then A78: ( ca in Ball (cb,(3 / 2)) & cb in Ball (ca,(3 / 2)) ) by METRIC_1:11;
V = W
proof
assume A79: V <> W ; ::_thesis: contradiction
Mn is_connected_in FX by A15, WELLORD1:def_5;
then ( [V,W] in Mn or [W,V] in Mn ) by A62, A71, A79, RELAT_2:def_6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A79, WELLORD1:1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A67, A76, A78, TARSKI:def_4;
then ( cb in PartUnion (W,Mn) or ca in PartUnion (V,Mn) ) by PCOMPS_2:def_1;
hence contradiction by A66, A75, XBOOLE_0:def_5; ::_thesis: verum
end;
hence A = B by A61, A70; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: A = B
then consider m being Nat such that
A80: n = m + 1 by NAT_1:6;
set r = 1 / (2 |^ n);
A81: 3 * (1 / (2 |^ n)) = (3 * 1) / (2 |^ n) by XCMPLX_1:74;
2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;
then ( 2 |^ n > 0 & 2 |^ (n + 1) >= 2 |^ n ) by PREPOWER:6, XREAL_1:151;
then 1 / (2 |^ (n + 1)) <= 1 / (2 |^ n) by XREAL_1:118;
then A82: dist (a,b) < 1 / (2 |^ n) by A58, XXREAL_0:2;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A in { (union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S1[V] } by A10, A48, A80;
then consider V being Subset of PM such that
A83: ( A = union { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S1[V] ) ;
consider Ba being set such that
A84: ( a in Ba & Ba in { H1(c,m) where c is Point of PM : ( S2[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) by A53, A83, TARSKI:def_4;
consider ca being Point of PM such that
A85: ( Ba = H1(ca,m) & S2[ca,V,m] & not ca in union { (union (Un . k)) where k is Element of NAT : k <= m } ) by A84;
dist (ca,a) < 1 / (2 |^ n) by A80, A84, A85, METRIC_1:11;
then A86: (dist (ca,a)) + (dist (a,b)) < (1 / (2 |^ n)) + (1 / (2 |^ n)) by A82, XREAL_1:8;
dist (ca,b) <= (dist (ca,a)) + (dist (a,b)) by METRIC_1:4;
then A87: dist (ca,b) < (1 / (2 |^ n)) + (1 / (2 |^ n)) by A86, XXREAL_0:2;
B in { (union { H1(c,m) where c is Point of PM : ( S2[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where W is Subset of PM : S1[W] } by A10, A49, A80;
then consider W being Subset of PM such that
A88: ( B = union { H1(c,m) where c is Point of PM : ( S2[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S1[W] ) ;
consider Bb being set such that
A89: ( b in Bb & Bb in { H1(c,m) where c is Point of PM : ( S2[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) by A55, A88, TARSKI:def_4;
consider cb being Point of PM such that
A90: ( Bb = H1(cb,m) & S2[cb,W,m] & not cb in union { (union (Un . k)) where k is Element of NAT : k <= m } ) by A89;
A91: dist (ca,cb) <= (dist (ca,b)) + (dist (b,cb)) by METRIC_1:4;
dist (cb,b) < 1 / (2 |^ n) by A80, A89, A90, METRIC_1:11;
then (dist (ca,b)) + (dist (b,cb)) < ((1 / (2 |^ n)) + (1 / (2 |^ n))) + (1 / (2 |^ n)) by A87, XREAL_1:8;
then dist (ca,cb) < 3 * (1 / (2 |^ n)) by A91, XXREAL_0:2;
then A92: ( ca in Ball (cb,(3 / (2 |^ (m + 1)))) & cb in Ball (ca,(3 / (2 |^ (m + 1)))) ) by A80, A81, METRIC_1:11;
V = W
proof
assume A93: V <> W ; ::_thesis: contradiction
Mn is_connected_in FX by A15, WELLORD1:def_5;
then ( [V,W] in Mn or [W,V] in Mn ) by A83, A88, A93, RELAT_2:def_6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A93, WELLORD1:1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A85, A90, A92, TARSKI:def_4;
then ( cb in PartUnion (W,Mn) or ca in PartUnion (V,Mn) ) by PCOMPS_2:def_1;
hence contradiction by A85, A90, XBOOLE_0:def_5; ::_thesis: verum
end;
hence A = B by A83, A88; ::_thesis: verum
end;
end;
end;
hence A = B ; ::_thesis: verum
end;
0 < 2 |^ (n + 2) by PREPOWER:6;
hence ( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) ) by A47, TBSP_1:11, XREAL_1:139; ::_thesis: verum
end;
hence Un9 . n is discrete by NAGATA_1:def_1; ::_thesis: verum
end;
hence Un9 is sigma_discrete by NAGATA_1:def_2; ::_thesis: verum
end;
theorem Th21: :: NAGATA_2:21
for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_discrete
proof
let T be non empty TopSpace; ::_thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_discrete )
assume A1: T is metrizable ; ::_thesis: ex Un being FamilySequence of T st Un is Basis_sigma_discrete
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 by A1, PCOMPS_1:def_8;
set bbcT = bool (bool the carrier of T);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;
deffunc H1( set ) -> set = { (Ball (x,(1 / (2 |^ (In ($1,NAT)))))) where x is Point of PM : x is Point of PM } ;
A4: for k being set st k in NAT holds
H1(k) in bool (bool the carrier of T)
proof
let k be set ; ::_thesis: ( k in NAT implies H1(k) in bool (bool the carrier of T) )
assume k in NAT ; ::_thesis: H1(k) in bool (bool the carrier of T)
then reconsider k = k as Element of NAT ;
H1(k) c= bool the carrier of T
proof
A5: In (k,NAT) = k by FUNCT_7:def_1;
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in H1(k) or B in bool the carrier of T )
assume B in H1(k) ; ::_thesis: B in bool the carrier of T
then ex x being Point of PM st
( B = Ball (x,(1 / (2 |^ k))) & x is Point of PM ) by A5;
then B in Family_open_set PM by PCOMPS_1:29;
hence B in bool the carrier of T by A3; ::_thesis: verum
end;
hence H1(k) in bool (bool the carrier of T) ; ::_thesis: verum
end;
consider FB being FamilySequence of T such that
A6: for k being set st k in NAT holds
FB . k = H1(k) from FUNCT_2:sch_2(A4);
defpred S1[ set , set ] means ex FS being FamilySequence of T st
( $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete );
set TPM = TopSpaceMetr PM;
A7: TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def_5;
then A8: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;
A9: for n being Element of NAT ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S1[n,Un]
proof
let n be Element of NAT ; ::_thesis: ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S1[n,Un]
A10: n = In (n,NAT) by FUNCT_7:def_1;
now__::_thesis:_for_U_being_Subset_of_T_st_U_in_FB_._n_holds_
U_is_open
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 H1(n) by A6;
then ex x being Point of PM st
( U = Ball (x,(1 / (2 |^ n))) & x is Point of PM ) by A10;
then U in the topology of T by A3, PCOMPS_1:29;
hence U is open by PRE_TOPC:def_2; ::_thesis: verum
end;
then A11: FB . n is open by TOPS_2:def_1;
A12: [#] (TopSpaceMetr PM) c= union (FB . n)
proof
let x be set ; :: 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 by A7;
2 |^ n > 0 by NEWTON:83;
then A13: x9 in Ball (x9,(1 / (2 |^ n))) by TBSP_1:11, XREAL_1:139;
Ball (x9,(1 / (2 |^ n))) in H1(n) by A10;
then Ball (x9,(1 / (2 |^ n))) in FB . n by A6;
hence x in union (FB . n) by A13, TARSKI:def_4; ::_thesis: verum
end;
union (FB . n) c= [#] (TopSpaceMetr PM)
proof
given x being set such that A14: x in union (FB . n) and
A15: not x in [#] (TopSpaceMetr PM) ; :: according to TARSKI:def_3 ::_thesis: contradiction
consider A being set such that
A16: x in A and
A17: A in FB . n by A14, TARSKI:def_4;
A in H1(n) by A6, A17;
then ex y being Point of PM st
( A = Ball (y,(1 / (2 |^ n))) & y is Point of PM ) by A10;
hence contradiction by A7, A15, A16; ::_thesis: verum
end;
then [#] (TopSpaceMetr PM) = union (FB . n) by A12, XBOOLE_0:def_10;
then FB . n is Cover of T by A8, SETFAM_1:45;
then consider Un being FamilySequence of T such that
A18: ( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB . n & Un is sigma_discrete ) by A1, A11, Th20;
Un in Funcs (NAT,(bool (bool the carrier of T))) by FUNCT_2:8;
hence ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S1[n,Un] by A18; ::_thesis: verum
end;
consider Un being Function of NAT,(Funcs (NAT,(bool (bool the carrier of T)))) such that
A19: for n being Element of NAT holds S1[n,Un . n] from FUNCT_2:sch_3(A9);
defpred S2[ set , set ] means for n, m being Element of NAT st PairFunc . [n,m] = $1 holds
for Unn being FamilySequence of T st Unn = Un . n holds
$2 = Unn . m;
A20: for k being set st k in NAT holds
ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] )
proof
let k be set ; ::_thesis: ( k in NAT implies ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] ) )
assume k in NAT ; ::_thesis: ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] )
then reconsider k9 = k as Element of NAT ;
NAT = rng PairFunc by Th2, FUNCT_2:def_3;
then consider nm being set such that
A21: nm in dom PairFunc and
A22: k9 = PairFunc . nm by FUNCT_1:def_3;
consider n, m being set such that
A23: n in NAT and
A24: m in NAT and
A25: nm = [n,m] by A21, ZFMISC_1:def_2;
reconsider Unn = Un . n as FamilySequence of T by A23, FUNCT_2:5, FUNCT_2:66;
take Ux = Unn . m; ::_thesis: ( Ux in bool (bool the carrier of T) & S2[k,Ux] )
dom Unn = NAT by PARTFUN1:def_2;
then m in dom Unn by A24;
then Ux in rng Unn by FUNCT_1:3;
hence Ux in bool (bool the carrier of T) ; ::_thesis: S2[k,Ux]
now__::_thesis:_for_n1,_m1_being_Element_of_NAT_st_PairFunc_._[n1,m1]_=_k_holds_
for_Unn_being_FamilySequence_of_T_st_Unn_=_Un_._n1_holds_
Ux_=_Unn_._m1
let n1, m1 be Element of NAT ; ::_thesis: ( PairFunc . [n1,m1] = k implies for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1 )
assume A26: PairFunc . [n1,m1] = k ; ::_thesis: for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1
now__::_thesis:_for_Unn_being_FamilySequence_of_T_st_Unn_=_Un_._n1_holds_
Ux_=_Unn_._m1
let Unn be FamilySequence of T; ::_thesis: ( Unn = Un . n1 implies Ux = Unn . m1 )
assume A27: Unn = Un . n1 ; ::_thesis: Ux = Unn . m1
A28: [n,m] = [n1,m1] by A21, A22, A25, A26, Th2, FUNCT_2:19;
then n1 = n by XTUPLE_0:1;
hence Ux = Unn . m1 by A27, A28, XTUPLE_0:1; ::_thesis: verum
end;
hence for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1 ; ::_thesis: verum
end;
hence S2[k,Ux] ; ::_thesis: verum
end;
consider UX being Function of NAT,(bool (bool the carrier of T)) such that
A29: for k being set st k in NAT holds
S2[k,UX . k] from FUNCT_2:sch_1(A20);
A30: 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 UX & p in B & B c= A )
proof
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 UX & 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 UX & p in B & B c= A )
then A31: 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 UX & p in B & B c= A ) )
assume A32: p in A ; ::_thesis: ex B being Subset of T st
( B in Union UX & p in B & B c= A )
reconsider p = p as Element of PM by A32, A31;
consider r being Real such that
A33: r > 0 and
A34: Ball (p,r) c= A by A32, A31, PCOMPS_1:def_4;
consider n being Element of NAT such that
A35: 1 / (2 |^ n) <= r by A33, PREPOWER:92;
consider Unn1 being FamilySequence of T such that
A36: Un . (n + 1) = Unn1 and
Union Unn1 is open and
A37: Union Unn1 is Cover of T and
A38: Union Unn1 is_finer_than FB . (n + 1) and
Unn1 is sigma_discrete by A19;
union (Union Unn1) = [#] T by A37, SETFAM_1:45;
then consider B being set such that
A39: p in B and
A40: B in Union Unn1 by TARSKI:def_4;
reconsider B = B as Subset of PM by A2, A40, PCOMPS_2:4;
consider B1 being set such that
A41: B1 in FB . (n + 1) and
A42: B c= B1 by A38, A40, SETFAM_1:def_2;
consider k being Element of NAT such that
A43: B in Unn1 . k by A40, PROB_1:12;
( n + 1 = In ((n + 1),NAT) & B1 in H1(n + 1) ) by A6, A41, FUNCT_7:def_1;
then consider q being Point of PM such that
A44: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and
q is Element of PM ;
now__::_thesis:_for_s_being_Element_of_PM_st_s_in_B_holds_
s_in_Ball_(p,r)
let s be Element of PM; ::_thesis: ( s in B implies s in Ball (p,r) )
assume s in B ; ::_thesis: s in Ball (p,r)
then A45: dist (q,s) < 1 / (2 |^ (n + 1)) by A42, A44, METRIC_1:11;
dist (q,p) < 1 / (2 |^ (n + 1)) by A39, A42, A44, METRIC_1:11;
then ( dist (p,s) <= (dist (q,p)) + (dist (q,s)) & (dist (q,p)) + (dist (q,s)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A45, METRIC_1:4, XREAL_1:8;
then dist (p,s) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;
then dist (p,s) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;
then dist (p,s) < 1 / (2 |^ n) by XCMPLX_1:92;
then dist (p,s) < r by A35, XXREAL_0:2;
hence s in Ball (p,r) by METRIC_1:11; ::_thesis: verum
end;
then A46: B c= Ball (p,r) by SUBSET_1:2;
UX . (PairFunc . [(n + 1),k]) = Unn1 . k by A29, A36;
then B in Union UX by A43, PROB_1:12;
hence ex B being Subset of T st
( B in Union UX & p in B & B c= A ) by A34, A39, A46, XBOOLE_1:1; ::_thesis: verum
end;
for k being Element of NAT holds UX . k is discrete
proof
let k be Element of NAT ; ::_thesis: UX . k is discrete
NAT = rng PairFunc by Th2, FUNCT_2:def_3;
then consider nm being set such that
A47: nm in dom PairFunc and
A48: k = PairFunc . nm by FUNCT_1:def_3;
consider n, m being set such that
A49: n in NAT and
A50: m in NAT and
A51: nm = [n,m] by A47, ZFMISC_1:def_2;
consider FS being FamilySequence of T such that
A52: Un . n = FS and
Union FS is open and
Union FS is Cover of T and
Union FS is_finer_than FB . n and
A53: FS is sigma_discrete by A19, A49;
dom FS = NAT by PARTFUN1:def_2;
then m in dom FS by A50;
then FS . m in rng FS by FUNCT_1:3;
then FS . m in bool (bool the carrier of T) ;
then reconsider FSm = FS . m as Subset-Family of T ;
FSm is discrete by A50, A53, NAGATA_1:def_2;
hence UX . k is discrete by A29, A48, A49, A50, A51, A52; ::_thesis: verum
end;
then A54: UX is sigma_discrete by NAGATA_1:def_2;
Union UX c= the topology of T
proof
let UXk be set ; :: according to TARSKI:def_3 ::_thesis: ( not UXk in Union UX or UXk in the topology of T )
assume UXk in Union UX ; ::_thesis: UXk in the topology of T
then consider k being Element of NAT such that
A55: UXk in UX . k by PROB_1:12;
reconsider UXk9 = UXk as Subset of T by A55;
NAT = rng PairFunc by Th2, FUNCT_2:def_3;
then consider nm being set such that
A56: nm in dom PairFunc and
A57: k = PairFunc . nm by FUNCT_1:def_3;
consider n, m being set such that
A58: n in NAT and
A59: m in NAT and
A60: nm = [n,m] by A56, ZFMISC_1:def_2;
reconsider Unn = Un . n as FamilySequence of T by A58, FUNCT_2:5, FUNCT_2:66;
UXk in Unn . m by A29, A55, A57, A58, A59, A60;
then A61: UXk in Union Unn by A59, PROB_1:12;
ex FS being FamilySequence of T st
( Un . n = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . n & FS is sigma_discrete ) by A19, A58;
then UXk9 is open by A61, TOPS_2:def_1;
hence UXk in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
then Union UX is Basis of T by A30, YELLOW_9:32;
then UX is Basis_sigma_discrete by A54, NAGATA_1:def_5;
hence ex Un being FamilySequence of T st Un is Basis_sigma_discrete ; ::_thesis: verum
end;
theorem :: NAGATA_2:22
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )
proof
let T be non empty TopSpace; ::_thesis: ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )
now__::_thesis:_(_T_is_regular_&_T_is_T_1_&_ex_Bn_being_FamilySequence_of_T_st_Bn_is_Basis_sigma_discrete_implies_T_is_metrizable_)
assume that
A1: ( T is regular & T is T_1 ) and
A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ; ::_thesis: T is metrizable
consider Bn being FamilySequence of T such that
A3: Bn is Basis_sigma_discrete by A2;
Bn is sigma_discrete by A3, NAGATA_1:def_5;
then A4: Bn is sigma_locally_finite by NAGATA_1:12;
Union Bn is Basis of T by A3, NAGATA_1:def_5;
then Bn is Basis_sigma_locally_finite by A4, NAGATA_1:def_6;
hence T is metrizable by A1, Th19; ::_thesis: verum
end;
hence ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable ) by Th21, NAGATA_1:15; ::_thesis: verum
end;