:: 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;