:: TBSP_1 semantic presentation begin theorem Th1: :: TBSP_1:1 for L being Real st 0 < L & L < 1 holds for n, m being Element of NAT st n <= m holds L to_power m <= L to_power n proof let L be Real; ::_thesis: ( 0 < L & L < 1 implies for n, m being Element of NAT st n <= m holds L to_power m <= L to_power n ) assume A1: ( 0 < L & L < 1 ) ; ::_thesis: for n, m being Element of NAT st n <= m holds L to_power m <= L to_power n let n, m be Element of NAT ; ::_thesis: ( n <= m implies L to_power m <= L to_power n ) assume A2: n <= m ; ::_thesis: L to_power m <= L to_power n percases ( n < m or n = m ) by A2, XXREAL_0:1; suppose n < m ; ::_thesis: L to_power m <= L to_power n hence L to_power m <= L to_power n by A1, POWER:40; ::_thesis: verum end; suppose n = m ; ::_thesis: L to_power m <= L to_power n hence L to_power m <= L to_power n ; ::_thesis: verum end; end; end; theorem Th2: :: TBSP_1:2 for L being Real st 0 < L & L < 1 holds for k being Element of NAT holds ( L to_power k <= 1 & 0 < L to_power k ) proof let L be Real; ::_thesis: ( 0 < L & L < 1 implies for k being Element of NAT holds ( L to_power k <= 1 & 0 < L to_power k ) ) assume that A1: 0 < L and A2: L < 1 ; ::_thesis: for k being Element of NAT holds ( L to_power k <= 1 & 0 < L to_power k ) defpred S1[ Element of NAT ] means ( L to_power \$1 <= 1 & 0 < L to_power \$1 ); A3: 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 that A4: L to_power k <= 1 and A5: 0 < L to_power k ; ::_thesis: S1[k + 1] A6: L to_power (k + 1) = (L to_power k) * (L to_power 1) by A1, POWER:27 .= (L to_power k) * L by POWER:25 ; (L to_power k) * L <= L to_power k by A2, A5, XREAL_1:153; hence S1[k + 1] by A1, A4, A5, A6, XREAL_1:129, XXREAL_0:2; ::_thesis: verum end; A7: S1[ 0 ] by POWER:24; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A3); ::_thesis: verum end; theorem Th3: :: TBSP_1:3 for L being Real st 0 < L & L < 1 holds for s being Real st 0 < s holds ex n being Element of NAT st L to_power n < s proof let L be Real; ::_thesis: ( 0 < L & L < 1 implies for s being Real st 0 < s holds ex n being Element of NAT st L to_power n < s ) assume A1: ( 0 < L & L < 1 ) ; ::_thesis: for s being Real st 0 < s holds ex n being Element of NAT st L to_power n < s let s be Real; ::_thesis: ( 0 < s implies ex n being Element of NAT st L to_power n < s ) deffunc H1( Element of NAT ) -> Element of REAL = L to_power (\$1 + 1); consider rseq being Real_Sequence such that A2: for n being Element of NAT holds rseq . n = H1(n) from SEQ_1:sch_1(); assume A3: 0 < s ; ::_thesis: ex n being Element of NAT st L to_power n < s ( rseq is convergent & lim rseq = 0 ) by A1, A2, SERIES_1:1; then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((rseq . m) - 0) < s by A3, SEQ_2:def_7; take n + 1 ; ::_thesis: L to_power (n + 1) < s A5: 0 < L to_power (n + 1) by A1, Th2; abs ((rseq . n) - 0) = abs (L to_power (n + 1)) by A2 .= L to_power (n + 1) by A5, ABSVALUE:def_1 ; hence L to_power (n + 1) < s by A4; ::_thesis: verum end; definition let N be non empty MetrStruct ; attrN is totally_bounded means :Def1: :: TBSP_1:def 1 for r being Real st r > 0 holds ex G being Subset-Family of N st ( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds ex w being Element of N st C = Ball (w,r) ) ); end; :: deftheorem Def1 defines totally_bounded TBSP_1:def_1_:_ for N being non empty MetrStruct holds ( N is totally_bounded iff for r being Real st r > 0 holds ex G being Subset-Family of N st ( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds ex w being Element of N st C = Ball (w,r) ) ) ); Lm1: for N being non empty MetrStruct for f being Function holds ( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) ) ) proof let N be non empty MetrStruct ; ::_thesis: for f being Function holds ( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) ) ) let f be Function; ::_thesis: ( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) ) ) thus ( f is sequence of N implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) implies f is sequence of N ) proof assume A1: f is sequence of N ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of N ) ) hence dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds f . x is Element of N let x be set ; ::_thesis: ( x in NAT implies f . x is Element of N ) assume x in NAT ; ::_thesis: f . x is Element of N then x in dom f by A1, FUNCT_2:def_1; then A2: f . x in rng f by FUNCT_1:def_3; rng f c= the carrier of N by A1, RELAT_1:def_19; hence f . x is Element of N by A2; ::_thesis: verum end; assume that A3: dom f = NAT and A4: for x being set st x in NAT holds f . x is Element of N ; ::_thesis: f is sequence of N now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_the_carrier_of_N let y be set ; ::_thesis: ( y in rng f implies y in the carrier of N ) assume y in rng f ; ::_thesis: y in the carrier of N then consider x being set such that A5: x in dom f and A6: y = f . x by FUNCT_1:def_3; f . x is Element of N by A3, A4, A5; hence y in the carrier of N by A6; ::_thesis: verum end; then rng f c= the carrier of N by TARSKI:def_3; hence f is sequence of N by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem :: TBSP_1:4 for N being non empty MetrStruct for f being Function holds ( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) ) proof let N be non empty MetrStruct ; ::_thesis: for f being Function holds ( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) ) let f be Function; ::_thesis: ( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) ) thus ( f is sequence of N implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) ) by Lm1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) implies f is sequence of N ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n is Element of N ; ::_thesis: f is sequence of N for x being set st x in NAT holds f . x is Element of N by A2; hence f is sequence of N by A1, Lm1; ::_thesis: verum end; definition let N be non empty MetrStruct ; let S2 be sequence of N; attrS2 is convergent means :Def2: :: TBSP_1:def 2 ex x being Element of N st for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),x) < r; end; :: deftheorem Def2 defines convergent TBSP_1:def_2_:_ for N being non empty MetrStruct for S2 being sequence of N holds ( S2 is convergent iff ex x being Element of N st for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),x) < r ); definition let M be non empty MetrSpace; let S1 be sequence of M; assume A1: S1 is convergent ; func lim S1 -> Element of M means :: TBSP_1:def 3 for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),it) < r; existence ex b1 being Element of M st for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b1) < r by A1, Def2; uniqueness for b1, b2 being Element of M st ( for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b1) < r ) & ( for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b2) < r ) holds b1 = b2 proof given g1, g2 being Element of M such that A2: for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S1 . m),g1) < r and A3: for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S1 . m),g2) < r and A4: g1 <> g2 ; ::_thesis: contradiction set a = (dist (g1,g2)) / 4; A5: dist (g1,g2) >= 0 by METRIC_1:5; A6: dist (g1,g2) <> 0 by A4, METRIC_1:2; then consider n1 being Element of NAT such that A7: for m being Element of NAT st n1 <= m holds dist ((S1 . m),g1) < (dist (g1,g2)) / 4 by A2, A5, XREAL_1:224; consider n2 being Element of NAT such that A8: for m being Element of NAT st n2 <= m holds dist ((S1 . m),g2) < (dist (g1,g2)) / 4 by A3, A6, A5, XREAL_1:224; set k = n1 + n2; A9: dist ((S1 . (n1 + n2)),g2) < (dist (g1,g2)) / 4 by A8, NAT_1:12; A10: dist (g1,g2) <= (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) by METRIC_1:4; dist ((S1 . (n1 + n2)),g1) < (dist (g1,g2)) / 4 by A7, NAT_1:12; then (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) < ((dist (g1,g2)) / 4) + ((dist (g1,g2)) / 4) by A9, XREAL_1:8; then dist (g1,g2) < (dist (g1,g2)) / 2 by A10, XXREAL_0:2; hence contradiction by A6, A5, XREAL_1:216; ::_thesis: verum end; end; :: deftheorem defines lim TBSP_1:def_3_:_ for M being non empty MetrSpace for S1 being sequence of M st S1 is convergent holds for b3 being Element of M holds ( b3 = lim S1 iff for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b3) < r ); definition let N be non empty MetrStruct ; let S2 be sequence of N; attrS2 is Cauchy means :Def4: :: TBSP_1:def 4 for r being Real st r > 0 holds ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r; end; :: deftheorem Def4 defines Cauchy TBSP_1:def_4_:_ for N being non empty MetrStruct for S2 being sequence of N holds ( S2 is Cauchy iff for r being Real st r > 0 holds ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r ); definition let N be non empty MetrStruct ; attrN is complete means :Def5: :: TBSP_1:def 5 for S2 being sequence of N st S2 is Cauchy holds S2 is convergent ; end; :: deftheorem Def5 defines complete TBSP_1:def_5_:_ for N being non empty MetrStruct holds ( N is complete iff for S2 being sequence of N st S2 is Cauchy holds S2 is convergent ); definition let N be non empty MetrStruct ; let S2 be sequence of N; let n be Element of NAT ; :: original: . redefine funcS2 . n -> Element of N; coherence S2 . n is Element of N proof thus S2 . n is Element of N ; ::_thesis: verum end; end; theorem Th5: :: TBSP_1:5 for N being non empty MetrStruct for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds S2 is Cauchy proof let N be non empty MetrStruct ; ::_thesis: for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds S2 is Cauchy let S2 be sequence of N; ::_thesis: ( N is triangle & N is symmetric & S2 is convergent implies S2 is Cauchy ) assume that A1: N is triangle and A2: N is symmetric ; ::_thesis: ( not S2 is convergent or S2 is Cauchy ) reconsider N = N as non empty symmetric MetrStruct by A2; assume A3: S2 is convergent ; ::_thesis: S2 is Cauchy reconsider S2 = S2 as sequence of N ; consider g being Element of N such that A4: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),g) < r by A3, Def2; let r be Real; :: according to TBSP_1:def_4 ::_thesis: ( r > 0 implies ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r ) assume 0 < r ; ::_thesis: ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds dist ((S2 . m),g) < r / 2 by A4, XREAL_1:215; take n ; ::_thesis: for n, m being Element of NAT st n <= n & n <= m holds dist ((S2 . n),(S2 . m)) < r let m, m9 be Element of NAT ; ::_thesis: ( n <= m & n <= m9 implies dist ((S2 . m),(S2 . m9)) < r ) assume that A6: m >= n and A7: m9 >= n ; ::_thesis: dist ((S2 . m),(S2 . m9)) < r A8: dist ((S2 . m9),g) < r / 2 by A5, A7; dist ((S2 . m),g) < r / 2 by A5, A6; then A9: (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) < (r / 2) + (r / 2) by A8, XREAL_1:8; dist ((S2 . m),(S2 . m9)) <= (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) by A1, METRIC_1:4; hence dist ((S2 . m),(S2 . m9)) < r by A9, XXREAL_0:2; ::_thesis: verum end; registration let M be non empty symmetric triangle MetrStruct ; cluster Function-like V33( NAT , the carrier of M) convergent -> Cauchy for Element of K10(K11(NAT, the carrier of M)); coherence for b1 being sequence of M st b1 is convergent holds b1 is Cauchy by Th5; end; theorem Th6: :: TBSP_1:6 for N being non empty symmetric MetrStruct for S2 being sequence of N holds ( S2 is Cauchy iff for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) proof let N be non empty symmetric MetrStruct ; ::_thesis: for S2 being sequence of N holds ( S2 is Cauchy iff for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) let S2 be sequence of N; ::_thesis: ( S2 is Cauchy iff for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) thus ( S2 is Cauchy implies for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) implies S2 is Cauchy ) proof assume A1: S2 is Cauchy ; ::_thesis: for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r let r be Real; ::_thesis: ( r > 0 implies ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) assume 0 < r ; ::_thesis: ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r then consider p being Element of NAT such that A2: for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r by A1, Def4; take p ; ::_thesis: for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r let n, k be Element of NAT ; ::_thesis: ( p <= n implies dist ((S2 . (n + k)),(S2 . n)) < r ) assume A3: p <= n ; ::_thesis: dist ((S2 . (n + k)),(S2 . n)) < r n <= n + k by NAT_1:11; then p <= n + k by A3, XXREAL_0:2; hence dist ((S2 . (n + k)),(S2 . n)) < r by A2, A3; ::_thesis: verum end; assume A4: for r being Real st r > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ; ::_thesis: S2 is Cauchy let r be Real; :: according to TBSP_1:def_4 ::_thesis: ( r > 0 implies ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r ) assume 0 < r ; ::_thesis: ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r then consider p being Element of NAT such that A5: for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r by A4; take p ; ::_thesis: for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r let n, m be Element of NAT ; ::_thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r ) assume that A6: p <= n and A7: p <= m ; ::_thesis: dist ((S2 . n),(S2 . m)) < r percases ( n <= m or m <= n ) ; suppose n <= m ; ::_thesis: dist ((S2 . n),(S2 . m)) < r then consider k being Nat such that A8: m = n + k by NAT_1:10; reconsider m9 = m, n9 = n, k = k as Element of NAT by ORDINAL1:def_12; m = n + k by A8; then dist ((S2 . m9),(S2 . n9)) < r by A5, A6; hence dist ((S2 . n),(S2 . m)) < r ; ::_thesis: verum end; suppose m <= n ; ::_thesis: dist ((S2 . n),(S2 . m)) < r then consider k being Nat such that A9: n = m + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; n = m + k by A9; hence dist ((S2 . n),(S2 . m)) < r by A5, A7; ::_thesis: verum end; end; end; theorem :: TBSP_1:7 for M being non empty MetrSpace for f being Contraction of M st M is complete holds ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) proof let M be non empty MetrSpace; ::_thesis: for f being Contraction of M st M is complete holds ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) let f be Contraction of M; ::_thesis: ( M is complete implies ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) ) consider L being Real such that A1: 0 < L and A2: L < 1 and A3: for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) by ALI2:def_1; A4: 1 - L > 0 by A2, XREAL_1:50; ex S1 being sequence of M st for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n) proof set z = the Element of M; deffunc H1( Nat, Element of M) -> Element of the carrier of M = f . \$2; ex h being Function of NAT, the carrier of M st ( h . 0 = the Element of M & ( for n being Nat holds h . (n + 1) = H1(n,h . n) ) ) from NAT_1:sch_12(); then consider h being Function of NAT, the carrier of M such that h . 0 = the Element of M and A5: for n being Nat holds h . (n + 1) = f . (h . n) ; take h ; ::_thesis: for n being Element of NAT holds h . (n + 1) = f . (h . n) let n be Element of NAT ; ::_thesis: h . (n + 1) = f . (h . n) thus h . (n + 1) = f . (h . n) by A5; ::_thesis: verum end; then consider S1 being sequence of M such that A6: for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n) ; set r = dist ((S1 . 1),(S1 . 0)); A7: 0 <= dist ((S1 . 1),(S1 . 0)) by METRIC_1:5; A8: 1 - L <> 0 by A2; assume A9: M is complete ; ::_thesis: ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) now__::_thesis:_ex_c_being_Element_of_M_st_ (_f_._c_=_c_&_(_for_y_being_Element_of_M_st_f_._y_=_y_holds_ y_=_c_)_) percases ( 0 = dist ((S1 . 1),(S1 . 0)) or 0 <> dist ((S1 . 1),(S1 . 0)) ) ; supposeA10: 0 = dist ((S1 . 1),(S1 . 0)) ; ::_thesis: ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) A11: f . (S1 . 0) = S1 . (0 + 1) by A6 .= S1 . 0 by A10, METRIC_1:2 ; for y being Element of M st f . y = y holds y = S1 . 0 proof let y be Element of M; ::_thesis: ( f . y = y implies y = S1 . 0 ) assume A12: f . y = y ; ::_thesis: y = S1 . 0 A13: dist (y,(S1 . 0)) >= 0 by METRIC_1:5; assume y <> S1 . 0 ; ::_thesis: contradiction then dist (y,(S1 . 0)) <> 0 by METRIC_1:2; then L * (dist (y,(S1 . 0))) < dist (y,(S1 . 0)) by A2, A13, XREAL_1:157; hence contradiction by A3, A11, A12; ::_thesis: verum end; hence ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) by A11; ::_thesis: verum end; supposeA14: 0 <> dist ((S1 . 1),(S1 . 0)) ; ::_thesis: ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) A15: for n being Element of NAT holds dist ((S1 . (n + 1)),(S1 . n)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power n) proof defpred S1[ Element of NAT ] means dist ((S1 . (\$1 + 1)),(S1 . \$1)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power \$1); A16: 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 dist ((S1 . (k + 1)),(S1 . k)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power k) ; ::_thesis: S1[k + 1] then A17: L * (dist ((S1 . (k + 1)),(S1 . k))) <= L * ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) by A1, XREAL_1:64; dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1))) = dist ((f . (S1 . (k + 1))),(S1 . (k + 1))) by A6 .= dist ((f . (S1 . (k + 1))),(f . (S1 . k))) by A6 ; then A18: dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1))) <= L * (dist ((S1 . (k + 1)),(S1 . k))) by A3; L * ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) = (dist ((S1 . 1),(S1 . 0))) * (L * (L to_power k)) .= (dist ((S1 . 1),(S1 . 0))) * ((L to_power k) * (L to_power 1)) by POWER:25 .= (dist ((S1 . 1),(S1 . 0))) * (L to_power (k + 1)) by A1, POWER:27 ; hence S1[k + 1] by A18, A17, XXREAL_0:2; ::_thesis: verum end; dist ((S1 . (0 + 1)),(S1 . 0)) = (dist ((S1 . 1),(S1 . 0))) * 1 .= (dist ((S1 . 1),(S1 . 0))) * (L to_power 0) by POWER:24 ; then A19: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A16); ::_thesis: verum end; A20: for k being Element of NAT holds dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) proof defpred S1[ Element of NAT ] means dist ((S1 . \$1),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power \$1)) / (1 - L)); A21: 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 A22: dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) ; ::_thesis: S1[k + 1] dist ((S1 . (k + 1)),(S1 . k)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power k) by A15; then A23: ( dist ((S1 . (k + 1)),(S1 . 0)) <= (dist ((S1 . (k + 1)),(S1 . k))) + (dist ((S1 . k),(S1 . 0))) & (dist ((S1 . (k + 1)),(S1 . k))) + (dist ((S1 . k),(S1 . 0))) <= ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) + ((dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L))) ) by A22, METRIC_1:4, XREAL_1:7; ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) + ((dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L))) = (dist ((S1 . 1),(S1 . 0))) * ((L to_power k) + ((1 - (L to_power k)) / (1 - L))) .= (dist ((S1 . 1),(S1 . 0))) * ((((L to_power k) / (1 - L)) * (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by A8, XCMPLX_1:87 .= (dist ((S1 . 1),(S1 . 0))) * ((((1 - L) * (L to_power k)) / (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by XCMPLX_1:74 .= (dist ((S1 . 1),(S1 . 0))) * ((((1 * (L to_power k)) - (L * (L to_power k))) + (1 - (L to_power k))) / (1 - L)) by XCMPLX_1:62 .= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L * (L to_power k))) / (1 - L)) .= (dist ((S1 . 1),(S1 . 0))) * ((1 - ((L to_power k) * (L to_power 1))) / (1 - L)) by POWER:25 .= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power (k + 1))) / (1 - L)) by A1, POWER:27 ; hence S1[k + 1] by A23, XXREAL_0:2; ::_thesis: verum end; (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power 0)) / (1 - L)) = (dist ((S1 . 1),(S1 . 0))) * ((1 - 1) / (1 - L)) by POWER:24 .= 0 ; then A24: S1[ 0 ] by METRIC_1:1; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A21); ::_thesis: verum end; A25: for k being Element of NAT holds dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L) proof let k be Element of NAT ; ::_thesis: dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L) 0 < L to_power k by A1, A2, Th2; then 1 - (L to_power k) <= 1 by XREAL_1:44; then (1 - (L to_power k)) / (1 - L) <= 1 / (1 - L) by A4, XREAL_1:72; then A26: (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) <= (dist ((S1 . 1),(S1 . 0))) * (1 / (1 - L)) by A7, XREAL_1:64; dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) by A20; then dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * (1 / (1 - L)) by A26, XXREAL_0:2; hence dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L) by XCMPLX_1:99; ::_thesis: verum end; A27: for n, k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) proof defpred S1[ Element of NAT ] means for k being Element of NAT holds dist ((S1 . (\$1 + k)),(S1 . \$1)) <= (L to_power \$1) * (dist ((S1 . k),(S1 . 0))); A28: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A29: for k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) ; ::_thesis: S1[n + 1] let k be Element of NAT ; ::_thesis: dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) A30: L * ((L to_power n) * (dist ((S1 . k),(S1 . 0)))) = (L * (L to_power n)) * (dist ((S1 . k),(S1 . 0))) .= ((L to_power n) * (L to_power 1)) * (dist ((S1 . k),(S1 . 0))) by POWER:25 .= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by A1, POWER:27 ; dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) = dist ((S1 . ((n + k) + 1)),(S1 . (n + 1))) .= dist ((f . (S1 . (n + k))),(S1 . (n + 1))) by A6 .= dist ((f . (S1 . (n + k))),(f . (S1 . n))) by A6 ; then A31: dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= L * (dist ((S1 . (n + k)),(S1 . n))) by A3; L * (dist ((S1 . (n + k)),(S1 . n))) <= L * ((L to_power n) * (dist ((S1 . k),(S1 . 0)))) by A1, A29, XREAL_1:64; hence dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by A31, A30, XXREAL_0:2; ::_thesis: verum end; A32: S1[ 0 ] proof let n be Element of NAT ; ::_thesis: dist ((S1 . (0 + n)),(S1 . 0)) <= (L to_power 0) * (dist ((S1 . n),(S1 . 0))) (L to_power 0) * (dist ((S1 . n),(S1 . 0))) = 1 * (dist ((S1 . n),(S1 . 0))) by POWER:24 .= dist ((S1 . n),(S1 . 0)) ; hence dist ((S1 . (0 + n)),(S1 . 0)) <= (L to_power 0) * (dist ((S1 . n),(S1 . 0))) ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A32, A28); ::_thesis: verum end; A33: for n, k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) proof let n, k be Element of NAT ; ::_thesis: dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) 0 <= L to_power n by A1, A2, Th2; then A34: (L to_power n) * (dist ((S1 . k),(S1 . 0))) <= (L to_power n) * ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) by A25, XREAL_1:64; dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) by A27; hence dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) by A34, XXREAL_0:2; ::_thesis: verum end; for s being Real st s > 0 holds ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S1 . (n + k)),(S1 . n)) < s proof A35: (1 - L) / (dist ((S1 . 1),(S1 . 0))) > 0 by A4, A7, A14, XREAL_1:139; let s be Real; ::_thesis: ( s > 0 implies ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S1 . (n + k)),(S1 . n)) < s ) assume s > 0 ; ::_thesis: ex p being Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S1 . (n + k)),(S1 . n)) < s then ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s > 0 by A35, XREAL_1:129; then consider p being Element of NAT such that A36: L to_power p < ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s by A1, A2, Th3; take p ; ::_thesis: for n, k being Element of NAT st p <= n holds dist ((S1 . (n + k)),(S1 . n)) < s let n, k be Element of NAT ; ::_thesis: ( p <= n implies dist ((S1 . (n + k)),(S1 . n)) < s ) assume p <= n ; ::_thesis: dist ((S1 . (n + k)),(S1 . n)) < s then L to_power n <= L to_power p by A1, A2, Th1; then A37: L to_power n < ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s by A36, XXREAL_0:2; (dist ((S1 . 1),(S1 . 0))) / (1 - L) > 0 by A4, A7, A14, XREAL_1:139; then A38: ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) < ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s) by A37, XREAL_1:68; A39: dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) by A33; ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s) = (((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * ((1 - L) / (dist ((S1 . 1),(S1 . 0))))) * s .= (((dist ((S1 . 1),(S1 . 0))) * (1 - L)) / ((dist ((S1 . 1),(S1 . 0))) * (1 - L))) * s by XCMPLX_1:76 .= 1 * s by A8, A14, XCMPLX_1:6, XCMPLX_1:60 .= s ; hence dist ((S1 . (n + k)),(S1 . n)) < s by A38, A39, XXREAL_0:2; ::_thesis: verum end; then S1 is Cauchy by Th6; then S1 is convergent by A9, Def5; then consider x being Element of M such that A40: for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S1 . m),x) < r by Def2; A41: f . x = x proof set a = (dist (x,(f . x))) / 4; assume x <> f . x ; ::_thesis: contradiction then A42: dist (x,(f . x)) <> 0 by METRIC_1:2; A43: dist (x,(f . x)) >= 0 by METRIC_1:5; then consider n being Element of NAT such that A44: for m being Element of NAT st n <= m holds dist ((S1 . m),x) < (dist (x,(f . x))) / 4 by A40, A42, XREAL_1:224; dist ((S1 . (n + 1)),(f . x)) = dist ((f . (S1 . n)),(f . x)) by A6; then A45: dist ((S1 . (n + 1)),(f . x)) <= L * (dist ((S1 . n),x)) by A3; A46: dist ((S1 . n),x) < (dist (x,(f . x))) / 4 by A44; L * (dist ((S1 . n),x)) <= dist ((S1 . n),x) by A2, METRIC_1:5, XREAL_1:153; then dist ((S1 . (n + 1)),(f . x)) <= dist ((S1 . n),x) by A45, XXREAL_0:2; then A47: dist ((S1 . (n + 1)),(f . x)) < (dist (x,(f . x))) / 4 by A46, XXREAL_0:2; A48: ( dist (x,(f . x)) <= (dist (x,(S1 . (n + 1)))) + (dist ((S1 . (n + 1)),(f . x))) & (dist (x,(f . x))) / 2 < dist (x,(f . x)) ) by A42, A43, METRIC_1:4, XREAL_1:216; dist (x,(S1 . (n + 1))) < (dist (x,(f . x))) / 4 by A44, NAT_1:11; then (dist (x,(S1 . (n + 1)))) + (dist ((S1 . (n + 1)),(f . x))) < ((dist (x,(f . x))) / 4) + ((dist (x,(f . x))) / 4) by A47, XREAL_1:8; hence contradiction by A48, XXREAL_0:2; ::_thesis: verum end; for y being Element of M st f . y = y holds y = x proof let y be Element of M; ::_thesis: ( f . y = y implies y = x ) assume A49: f . y = y ; ::_thesis: y = x A50: dist (y,x) >= 0 by METRIC_1:5; assume y <> x ; ::_thesis: contradiction then dist (y,x) <> 0 by METRIC_1:2; then L * (dist (y,x)) < dist (y,x) by A2, A50, XREAL_1:157; hence contradiction by A3, A41, A49; ::_thesis: verum end; hence ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) by A41; ::_thesis: verum end; end; end; hence ex c being Element of M st ( f . c = c & ( for y being Element of M st f . y = y holds y = c ) ) ; ::_thesis: verum end; theorem :: TBSP_1:8 for T being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr T is compact holds T is complete proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: ( TopSpaceMetr T is compact implies T is complete ) set TM = TopSpaceMetr T; A1: TopSpaceMetr T = TopStruct(# the carrier of T,(Family_open_set T) #) by PCOMPS_1:def_5; assume A2: TopSpaceMetr T is compact ; ::_thesis: T is complete let S2 be sequence of T; :: according to TBSP_1:def_5 ::_thesis: ( S2 is Cauchy implies S2 is convergent ) assume A3: S2 is Cauchy ; ::_thesis: S2 is convergent S2 is convergent proof A4: for p being Element of NAT holds { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } <> {} proof let p be Element of NAT ; ::_thesis: { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } <> {} S2 . p in { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } ; hence { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } <> {} ; ::_thesis: verum end; defpred S1[ Subset of (TopSpaceMetr T)] means ex p being Element of NAT st \$1 = { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } ; consider F being Subset-Family of (TopSpaceMetr T) such that A5: for B being Subset of (TopSpaceMetr T) holds ( B in F iff S1[B] ) from SUBSET_1:sch_3(); defpred S2[ Point of T] means ex n being Element of NAT st ( 0 <= n & \$1 = S2 . n ); set B0 = { x where x is Point of T : S2[x] } ; A6: { x where x is Point of T : S2[x] } is Subset of T from DOMAIN_1:sch_7(); then A7: { x where x is Point of T : S2[x] } in F by A1, A5; reconsider B0 = { x where x is Point of T : S2[x] } as Subset of (TopSpaceMetr T) by A1, A6; reconsider F = F as Subset-Family of (TopSpaceMetr T) ; set G = clf F; A8: Cl B0 in clf F by A7, PCOMPS_1:def_2; A9: clf F is centered proof thus clf F <> {} by A8; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds ( b1 = {} or not b1 c= clf F or not b1 is finite or not meet b1 = {} ) let H be set ; ::_thesis: ( H = {} or not H c= clf F or not H is finite or not meet H = {} ) assume that A10: H <> {} and A11: H c= clf F and A12: H is finite ; ::_thesis: not meet H = {} A13: H c= bool the carrier of (TopSpaceMetr T) by A11, XBOOLE_1:1; H is c=-linear proof let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in H or not C in H or B,C are_c=-comparable ) assume that A14: B in H and A15: C in H ; ::_thesis: B,C are_c=-comparable reconsider B = B, C = C as Subset of (TopSpaceMetr T) by A13, A14, A15; consider V being Subset of (TopSpaceMetr T) such that A16: B = Cl V and A17: V in F by A11, A14, PCOMPS_1:def_2; consider p being Element of NAT such that A18: V = { x where x is Point of T : ex n being Element of NAT st ( p <= n & x = S2 . n ) } by A5, A17; consider W being Subset of (TopSpaceMetr T) such that A19: C = Cl W and A20: W in F by A11, A15, PCOMPS_1:def_2; consider q being Element of NAT such that A21: W = { x where x is Point of T : ex n being Element of NAT st ( q <= n & x = S2 . n ) } by A5, A20; now__::_thesis:_(_(_q_<=_p_&_V_c=_W_)_or_(_p_<=_q_&_W_c=_V_)_) percases ( q <= p or p <= q ) ; caseA22: q <= p ; ::_thesis: V c= W thus V c= W ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in V or y in W ) assume y in V ; ::_thesis: y in W then consider x being Point of T such that A23: y = x and A24: ex n being Element of NAT st ( p <= n & x = S2 . n ) by A18; consider n being Element of NAT such that A25: p <= n and A26: x = S2 . n by A24; q <= n by A22, A25, XXREAL_0:2; hence y in W by A21, A23, A26; ::_thesis: verum end; end; caseA27: p <= q ; ::_thesis: W c= V thus W c= V ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in W or y in V ) assume y in W ; ::_thesis: y in V then consider x being Point of T such that A28: y = x and A29: ex n being Element of NAT st ( q <= n & x = S2 . n ) by A21; consider n being Element of NAT such that A30: q <= n and A31: x = S2 . n by A29; p <= n by A27, A30, XXREAL_0:2; hence y in V by A18, A28, A31; ::_thesis: verum end; end; end; end; then ( B c= C or C c= B ) by A16, A19, PRE_TOPC:19; hence B,C are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum end; then consider m being set such that A32: m in H and A33: for C being set st C in H holds m c= C by A10, A12, FINSET_1:11; A34: m c= meet H by A10, A33, SETFAM_1:5; reconsider m = m as Subset of (TopSpaceMetr T) by A13, A32; consider A being Subset of (TopSpaceMetr T) such that A35: m = Cl A and A36: A in F by A11, A32, PCOMPS_1:def_2; A <> {} by A5, A4, A36; then m <> {} by A35, PRE_TOPC:18, XBOOLE_1:3; hence not meet H = {} by A34; ::_thesis: verum end; clf F is closed by PCOMPS_1:11; then meet (clf F) <> {} by A2, A9, COMPTS_1:4; then consider c being Point of (TopSpaceMetr T) such that A37: c in meet (clf F) by SUBSET_1:4; reconsider c = c as Point of T by A1; take c ; :: according to TBSP_1:def_2 ::_thesis: for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),c) < r let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),c) < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),c) < r then A38: 0 < r / 2 by XREAL_1:215; then consider p being Element of NAT such that A39: for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r / 2 by A3, Def4; dist (c,c) < r / 2 by A38, METRIC_1:1; then A40: c in Ball (c,(r / 2)) by METRIC_1:11; reconsider Z = Ball (c,(r / 2)) as Subset of (TopSpaceMetr T) by A1; Ball (c,(r / 2)) in Family_open_set T by PCOMPS_1:29; then A41: Z is open by A1, PRE_TOPC:def_2; defpred S3[ set ] means ex n being Element of NAT st ( p <= n & \$1 = S2 . n ); set B = { x where x is Point of T : S3[x] } ; A42: { x where x is Point of T : S3[x] } is Subset of T from DOMAIN_1:sch_7(); then A43: { x where x is Point of T : S3[x] } in F by A1, A5; reconsider B = { x where x is Point of T : S3[x] } as Subset of (TopSpaceMetr T) by A1, A42; Cl B in clf F by A43, PCOMPS_1:def_2; then c in Cl B by A37, SETFAM_1:def_1; then B meets Z by A40, A41, PRE_TOPC:def_7; then consider g being set such that A44: g in B /\ Z by XBOOLE_0:4; take p ; ::_thesis: for m being Element of NAT st p <= m holds dist ((S2 . m),c) < r let m be Element of NAT ; ::_thesis: ( p <= m implies dist ((S2 . m),c) < r ) A45: g in B by A44, XBOOLE_0:def_4; A46: g in Z by A44, XBOOLE_0:def_4; then reconsider g = g as Point of T ; consider x being Point of T such that A47: g = x and A48: ex n being Element of NAT st ( p <= n & x = S2 . n ) by A45; consider n being Element of NAT such that A49: p <= n and A50: x = S2 . n by A48; assume p <= m ; ::_thesis: dist ((S2 . m),c) < r then A51: dist ((S2 . m),(S2 . n)) < r / 2 by A39, A49; dist ((S2 . n),c) < r / 2 by A46, A47, A50, METRIC_1:11; then A52: (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) < (r / 2) + (r / 2) by A51, XREAL_1:8; dist ((S2 . m),c) <= (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) by METRIC_1:4; hence dist ((S2 . m),c) < r by A52, XXREAL_0:2; ::_thesis: verum end; hence S2 is convergent ; ::_thesis: verum end; theorem :: TBSP_1:9 for N being non empty MetrStruct st N is Reflexive & N is triangle & TopSpaceMetr N is compact holds N is totally_bounded proof let N be non empty MetrStruct ; ::_thesis: ( N is Reflexive & N is triangle & TopSpaceMetr N is compact implies N is totally_bounded ) assume A1: N is Reflexive ; ::_thesis: ( not N is triangle or not TopSpaceMetr N is compact or N is totally_bounded ) set TM = TopSpaceMetr N; assume A2: N is triangle ; ::_thesis: ( not TopSpaceMetr N is compact or N is totally_bounded ) assume A3: TopSpaceMetr N is compact ; ::_thesis: N is totally_bounded let r be Real; :: according to TBSP_1:def_1 ::_thesis: ( r > 0 implies ex G being Subset-Family of N st ( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds ex w being Element of N st C = Ball (w,r) ) ) ) assume A4: r > 0 ; ::_thesis: ex G being Subset-Family of N st ( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds ex w being Element of N st C = Ball (w,r) ) ) defpred S1[ Subset of N] means ex x being Element of N st \$1 = Ball (x,r); consider G being Subset-Family of N such that A5: for C being Subset of N holds ( C in G iff S1[C] ) from SUBSET_1:sch_3(); A6: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5; then reconsider G = G as Subset-Family of (TopSpaceMetr N) ; for x being Element of (TopSpaceMetr N) holds x in union G proof let x be Element of (TopSpaceMetr N); ::_thesis: x in union G reconsider x = x as Element of N by A6; dist (x,x) = 0 by A1, METRIC_1:1; then A7: x in Ball (x,r) by A4, METRIC_1:11; Ball (x,r) in G by A5; hence x in union G by A7, TARSKI:def_4; ::_thesis: verum end; then [#] (TopSpaceMetr N) = union G by SUBSET_1:28; then A8: G is Cover of (TopSpaceMetr N) by SETFAM_1:45; for C being Subset of (TopSpaceMetr N) st C in G holds C is open proof let C be Subset of (TopSpaceMetr N); ::_thesis: ( C in G implies C is open ) assume A9: C in G ; ::_thesis: C is open reconsider C = C as Subset of N by A6; ex x being Element of N st C = Ball (x,r) by A5, A9; then C in the topology of (TopSpaceMetr N) by A2, A6, PCOMPS_1:29; hence C is open by PRE_TOPC:def_2; ::_thesis: verum end; then G is open by TOPS_2:def_1; then consider H being Subset-Family of (TopSpaceMetr N) such that A10: H c= G and A11: H is Cover of (TopSpaceMetr N) and A12: H is finite by A3, A8, COMPTS_1:def_1; reconsider H = H as Subset-Family of N by A6; take H ; ::_thesis: ( H is finite & the carrier of N = union H & ( for C being Subset of N st C in H holds ex w being Element of N st C = Ball (w,r) ) ) union H = the carrier of (TopSpaceMetr N) by A11, SETFAM_1:45; hence ( H is finite & the carrier of N = union H & ( for C being Subset of N st C in H holds ex w being Element of N st C = Ball (w,r) ) ) by A6, A5, A10, A12; ::_thesis: verum end; definition let N be non empty MetrStruct ; attrN is bounded means :Def6: :: TBSP_1:def 6 ex r being Real st ( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ); let C be Subset of N; attrC is bounded means :Def7: :: TBSP_1:def 7 ex r being Real st ( 0 < r & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r ) ); end; :: deftheorem Def6 defines bounded TBSP_1:def_6_:_ for N being non empty MetrStruct holds ( N is bounded iff ex r being Real st ( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) ); :: deftheorem Def7 defines bounded TBSP_1:def_7_:_ for N being non empty MetrStruct for C being Subset of N holds ( C is bounded iff ex r being Real st ( 0 < r & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r ) ) ); registration let A be non empty set ; cluster DiscreteSpace A -> bounded ; coherence DiscreteSpace A is bounded proof take 2 ; :: according to TBSP_1:def_6 ::_thesis: ( 0 < 2 & ( for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2 ) ) set N = DiscreteSpace A; thus 0 < 2 ; ::_thesis: for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2 let x, y be Point of (DiscreteSpace A); ::_thesis: dist (x,y) <= 2 A1: ( DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #) & dist (x,y) = the distance of (DiscreteSpace A) . (x,y) ) by METRIC_1:def_1, METRIC_1:def_11; ( x = y or x <> y ) ; then ( dist (x,y) = 0 or dist (x,y) = 1 ) by A1, METRIC_1:def_10; hence dist (x,y) <= 2 ; ::_thesis: verum end; end; registration cluster non empty Reflexive discerning symmetric triangle Discerning bounded for MetrStruct ; existence ex b1 being non empty MetrSpace st b1 is bounded proof take DiscreteSpace {0} ; ::_thesis: DiscreteSpace {0} is bounded thus DiscreteSpace {0} is bounded ; ::_thesis: verum end; end; registration let N be non empty MetrStruct ; cluster empty -> bounded for Element of K10( the carrier of N); coherence for b1 being Subset of N st b1 is empty holds b1 is bounded proof let S be Subset of N; ::_thesis: ( S is empty implies S is bounded ) assume A1: S is empty ; ::_thesis: S is bounded take 1 ; :: according to TBSP_1:def_7 ::_thesis: ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds dist (x,y) <= 1 ) ) thus ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds dist (x,y) <= 1 ) ) by A1; ::_thesis: verum end; end; registration let N be non empty MetrStruct ; cluster bounded for Element of K10( the carrier of N); existence ex b1 being Subset of N st b1 is bounded proof take {} N ; ::_thesis: {} N is bounded thus {} N is bounded ; ::_thesis: verum end; end; theorem Th10: :: TBSP_1:10 for N being non empty MetrStruct for C being Subset of N holds ( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st ( 0 < r & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) implies C is bounded ) ) proof let N be non empty MetrStruct ; ::_thesis: for C being Subset of N holds ( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st ( 0 < r & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) implies C is bounded ) ) let C be Subset of N; ::_thesis: ( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st ( 0 < r & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) implies C is bounded ) ) thus ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) ) ::_thesis: ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st ( 0 < r & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) implies C is bounded ) proof set w = the Element of C; assume A1: C <> {} ; ::_thesis: ( not C is bounded or ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) ) then reconsider w = the Element of C as Point of N by TARSKI:def_3; assume C is bounded ; ::_thesis: ex r being Real ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) then consider r being Real such that A2: 0 < r and A3: for x, y being Point of N st x in C & y in C holds dist (x,y) <= r by Def7; take r ; ::_thesis: ex w being Element of N st ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) take w ; ::_thesis: ( 0 < r & w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) thus 0 < r by A2; ::_thesis: ( w in C & ( for z being Point of N st z in C holds dist (w,z) <= r ) ) thus w in C by A1; ::_thesis: for z being Point of N st z in C holds dist (w,z) <= r let z be Point of N; ::_thesis: ( z in C implies dist (w,z) <= r ) assume z in C ; ::_thesis: dist (w,z) <= r hence dist (w,z) <= r by A3; ::_thesis: verum end; assume A4: N is symmetric ; ::_thesis: ( not N is triangle or for r being Real for w being Element of N holds ( not 0 < r or ex z being Point of N st ( z in C & not dist (w,z) <= r ) ) or C is bounded ) assume A5: N is triangle ; ::_thesis: ( for r being Real for w being Element of N holds ( not 0 < r or ex z being Point of N st ( z in C & not dist (w,z) <= r ) ) or C is bounded ) given r being Real, w being Element of N such that A6: 0 < r and A7: for z being Point of N st z in C holds dist (w,z) <= r ; ::_thesis: C is bounded set s = r + r; reconsider N = N as symmetric MetrStruct by A4; reconsider w = w as Element of N ; ex s being Real st ( 0 < s & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) ) proof take r + r ; ::_thesis: ( 0 < r + r & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r + r ) ) thus 0 < r + r by A6; ::_thesis: for x, y being Point of N st x in C & y in C holds dist (x,y) <= r + r let x, y be Point of N; ::_thesis: ( x in C & y in C implies dist (x,y) <= r + r ) assume that A8: x in C and A9: y in C ; ::_thesis: dist (x,y) <= r + r A10: dist (w,x) <= r by A7, A8; dist (w,y) <= r by A7, A9; then A11: (dist (x,w)) + (dist (w,y)) <= r + r by A10, XREAL_1:7; dist (x,y) <= (dist (x,w)) + (dist (w,y)) by A5, METRIC_1:4; hence dist (x,y) <= r + r by A11, XXREAL_0:2; ::_thesis: verum end; hence C is bounded by Def7; ::_thesis: verum end; theorem Th11: :: TBSP_1:11 for N being non empty MetrStruct for w being Element of N for r being real number st N is Reflexive & 0 < r holds w in Ball (w,r) proof let N be non empty MetrStruct ; ::_thesis: for w being Element of N for r being real number st N is Reflexive & 0 < r holds w in Ball (w,r) let w be Element of N; ::_thesis: for r being real number st N is Reflexive & 0 < r holds w in Ball (w,r) let r be real number ; ::_thesis: ( N is Reflexive & 0 < r implies w in Ball (w,r) ) assume N is Reflexive ; ::_thesis: ( not 0 < r or w in Ball (w,r) ) then A1: dist (w,w) = 0 by METRIC_1:1; assume 0 < r ; ::_thesis: w in Ball (w,r) hence w in Ball (w,r) by A1, METRIC_1:11; ::_thesis: verum end; theorem Th12: :: TBSP_1:12 for T being non empty Reflexive symmetric triangle MetrStruct for t1 being Element of T for r being real number st r <= 0 holds Ball (t1,r) = {} proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T for r being real number st r <= 0 holds Ball (t1,r) = {} let t1 be Element of T; ::_thesis: for r being real number st r <= 0 holds Ball (t1,r) = {} let r be real number ; ::_thesis: ( r <= 0 implies Ball (t1,r) = {} ) assume A1: r <= 0 ; ::_thesis: Ball (t1,r) = {} set c = the Element of Ball (t1,r); assume A2: Ball (t1,r) <> {} ; ::_thesis: contradiction then reconsider c = the Element of Ball (t1,r) as Point of T by TARSKI:def_3; dist (t1,c) < r by A2, METRIC_1:11; hence contradiction by A1, METRIC_1:5; ::_thesis: verum end; Lm2: for T being non empty Reflexive symmetric triangle MetrStruct for t1 being Element of T for r being real number st 0 < r holds Ball (t1,r) is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T for r being real number st 0 < r holds Ball (t1,r) is bounded let t1 be Element of T; ::_thesis: for r being real number st 0 < r holds Ball (t1,r) is bounded let r be real number ; ::_thesis: ( 0 < r implies Ball (t1,r) is bounded ) assume A1: 0 < r ; ::_thesis: Ball (t1,r) is bounded set P = Ball (t1,r); reconsider r = r as Real by XREAL_0:def_1; ex r being Real ex t1 being Element of T st ( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds dist (t1,z) <= r ) ) proof take r ; ::_thesis: ex t1 being Element of T st ( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds dist (t1,z) <= r ) ) take t1 ; ::_thesis: ( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds dist (t1,z) <= r ) ) thus 0 < r by A1; ::_thesis: ( t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds dist (t1,z) <= r ) ) thus t1 in Ball (t1,r) by A1, Th11; ::_thesis: for z being Point of T st z in Ball (t1,r) holds dist (t1,z) <= r let z be Point of T; ::_thesis: ( z in Ball (t1,r) implies dist (t1,z) <= r ) assume z in Ball (t1,r) ; ::_thesis: dist (t1,z) <= r hence dist (t1,z) <= r by METRIC_1:11; ::_thesis: verum end; hence Ball (t1,r) is bounded by Th10; ::_thesis: verum end; registration let T be non empty Reflexive symmetric triangle MetrStruct ; let t1 be Element of T; let r be real number ; cluster Ball (t1,r) -> bounded ; coherence Ball (t1,r) is bounded proof percases ( r <= 0 or 0 < r ) ; suppose r <= 0 ; ::_thesis: Ball (t1,r) is bounded then Ball (t1,r) = {} T by Th12; hence Ball (t1,r) is bounded ; ::_thesis: verum end; suppose 0 < r ; ::_thesis: Ball (t1,r) is bounded hence Ball (t1,r) is bounded by Lm2; ::_thesis: verum end; end; end; end; theorem Th13: :: TBSP_1:13 for T being non empty Reflexive symmetric triangle MetrStruct for P, Q being Subset of T st P is bounded & Q is bounded holds P \/ Q is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P, Q being Subset of T st P is bounded & Q is bounded holds P \/ Q is bounded let P, Q be Subset of T; ::_thesis: ( P is bounded & Q is bounded implies P \/ Q is bounded ) assume that A1: P is bounded and A2: Q is bounded ; ::_thesis: P \/ Q is bounded percases ( P = {} or P <> {} ) ; suppose P = {} ; ::_thesis: P \/ Q is bounded hence P \/ Q is bounded by A2; ::_thesis: verum end; supposeA3: P <> {} ; ::_thesis: P \/ Q is bounded now__::_thesis:_P_\/_Q_is_bounded percases ( Q = {} or Q <> {} ) ; suppose Q = {} ; ::_thesis: P \/ Q is bounded hence P \/ Q is bounded by A1; ::_thesis: verum end; suppose Q <> {} ; ::_thesis: P \/ Q is bounded then consider s being Real, d being Element of T such that A4: 0 < s and d in Q and A5: for z being Point of T st z in Q holds dist (d,z) <= s by A2, Th10; consider r being Real, t1 being Element of T such that A6: 0 < r and A7: t1 in P and A8: for z being Point of T st z in P holds dist (t1,z) <= r by A1, A3, Th10; set t = (r + s) + (dist (t1,d)); A9: 0 <= dist (t1,d) by METRIC_1:5; then A10: r < r + ((dist (t1,d)) + s) by A4, XREAL_1:29; ex t being Real ex t1 being Element of T st ( 0 < t & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds dist (t1,z) <= t ) ) proof take (r + s) + (dist (t1,d)) ; ::_thesis: ex t1 being Element of T st ( 0 < (r + s) + (dist (t1,d)) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds dist (t1,z) <= (r + s) + (dist (t1,d)) ) ) take t1 ; ::_thesis: ( 0 < (r + s) + (dist (t1,d)) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds dist (t1,z) <= (r + s) + (dist (t1,d)) ) ) thus 0 < (r + s) + (dist (t1,d)) by A6, A4, A9; ::_thesis: ( t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds dist (t1,z) <= (r + s) + (dist (t1,d)) ) ) thus t1 in P \/ Q by A7, XBOOLE_0:def_3; ::_thesis: for z being Point of T st z in P \/ Q holds dist (t1,z) <= (r + s) + (dist (t1,d)) let z be Point of T; ::_thesis: ( z in P \/ Q implies dist (t1,z) <= (r + s) + (dist (t1,d)) ) assume z in P \/ Q ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d)) then A11: ( z in P or z in Q ) by XBOOLE_0:def_3; now__::_thesis:_dist_(t1,z)_<=_(r_+_s)_+_(dist_(t1,d)) percases ( dist (t1,z) <= r or dist (d,z) <= s ) by A8, A5, A11; suppose dist (t1,z) <= r ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d)) hence dist (t1,z) <= (r + s) + (dist (t1,d)) by A10, XXREAL_0:2; ::_thesis: verum end; suppose dist (d,z) <= s ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d)) then ( dist (t1,z) <= (dist (t1,d)) + (dist (d,z)) & (dist (t1,d)) + (dist (d,z)) <= (dist (t1,d)) + s ) by METRIC_1:4, XREAL_1:7; then A12: dist (t1,z) <= (dist (t1,d)) + s by XXREAL_0:2; (dist (t1,d)) + s <= r + ((dist (t1,d)) + s) by A6, XREAL_1:29; hence dist (t1,z) <= (r + s) + (dist (t1,d)) by A12, XXREAL_0:2; ::_thesis: verum end; end; end; hence dist (t1,z) <= (r + s) + (dist (t1,d)) ; ::_thesis: verum end; hence P \/ Q is bounded by Th10; ::_thesis: verum end; end; end; hence P \/ Q is bounded ; ::_thesis: verum end; end; end; theorem Th14: :: TBSP_1:14 for N being non empty MetrStruct for C, D being Subset of N st C is bounded & D c= C holds D is bounded proof let N be non empty MetrStruct ; ::_thesis: for C, D being Subset of N st C is bounded & D c= C holds D is bounded let C, D be Subset of N; ::_thesis: ( C is bounded & D c= C implies D is bounded ) assume that A1: C is bounded and A2: D c= C ; ::_thesis: D is bounded consider r being Real such that A3: 0 < r and A4: for x, y being Point of N st x in C & y in C holds dist (x,y) <= r by A1, Def7; ex r being Real st ( 0 < r & ( for x, y being Point of N st x in D & y in D holds dist (x,y) <= r ) ) proof take r ; ::_thesis: ( 0 < r & ( for x, y being Point of N st x in D & y in D holds dist (x,y) <= r ) ) thus 0 < r by A3; ::_thesis: for x, y being Point of N st x in D & y in D holds dist (x,y) <= r let x, y be Point of N; ::_thesis: ( x in D & y in D implies dist (x,y) <= r ) assume ( x in D & y in D ) ; ::_thesis: dist (x,y) <= r hence dist (x,y) <= r by A2, A4; ::_thesis: verum end; hence D is bounded by Def7; ::_thesis: verum end; theorem Th15: :: TBSP_1:15 for T being non empty Reflexive symmetric triangle MetrStruct for t1 being Element of T for P being Subset of T st P = {t1} holds P is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T for P being Subset of T st P = {t1} holds P is bounded let t1 be Element of T; ::_thesis: for P being Subset of T st P = {t1} holds P is bounded let P be Subset of T; ::_thesis: ( P = {t1} implies P is bounded ) assume A1: P = {t1} ; ::_thesis: P is bounded {t1} is Subset of (Ball (t1,1)) by Th11, SUBSET_1:41; hence P is bounded by A1, Th14; ::_thesis: verum end; theorem Th16: :: TBSP_1:16 for T being non empty Reflexive symmetric triangle MetrStruct for P being Subset of T st P is finite holds P is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P being Subset of T st P is finite holds P is bounded let P be Subset of T; ::_thesis: ( P is finite implies P is bounded ) defpred S1[ set ] means ex X being Subset of T st ( X = \$1 & X is bounded ); {} T is bounded ; then A1: S1[ {} ] ; A2: for x, B being set st x in P & B c= P & S1[B] holds S1[B \/ {x}] proof let x, B be set ; ::_thesis: ( x in P & B c= P & S1[B] implies S1[B \/ {x}] ) assume that A3: x in P and B c= P and A4: S1[B] ; ::_thesis: S1[B \/ {x}] reconsider x = x as Element of T by A3; reconsider W = {x} as Subset of T ; consider X being Subset of T such that A5: ( X = B & X is bounded ) by A4; A6: W is bounded by Th15; ex Y being Subset of T st ( Y = B \/ {x} & Y is bounded ) proof take X \/ W ; ::_thesis: ( X \/ W = B \/ {x} & X \/ W is bounded ) thus ( X \/ W = B \/ {x} & X \/ W is bounded ) by A5, A6, Th13; ::_thesis: verum end; hence S1[B \/ {x}] ; ::_thesis: verum end; assume A7: P is finite ; ::_thesis: P is bounded S1[P] from FINSET_1:sch_2(A7, A1, A2); hence P is bounded ; ::_thesis: verum end; registration let T be non empty Reflexive symmetric triangle MetrStruct ; cluster finite -> bounded for Element of K10( the carrier of T); coherence for b1 being Subset of T st b1 is finite holds b1 is bounded by Th16; end; registration let T be non empty Reflexive symmetric triangle MetrStruct ; cluster non empty finite for Element of K10( the carrier of T); existence ex b1 being Subset of T st ( b1 is finite & not b1 is empty ) proof take the non empty finite Subset of T ; ::_thesis: ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty ) thus ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty ) ; ::_thesis: verum end; end; theorem Th17: :: TBSP_1:17 for T being non empty Reflexive symmetric triangle MetrStruct for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds P is bounded ) holds union Y is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds P is bounded ) holds union Y is bounded let Y be Subset-Family of T; ::_thesis: ( Y is finite & ( for P being Subset of T st P in Y holds P is bounded ) implies union Y is bounded ) assume that A1: Y is finite and A2: for P being Subset of T st P in Y holds P is bounded ; ::_thesis: union Y is bounded defpred S1[ set ] means ex X being Subset of T st ( X = union \$1 & X is bounded ); A3: for x, B being set st x in Y & B c= Y & S1[B] holds S1[B \/ {x}] proof let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] ) assume that A4: x in Y and B c= Y and A5: S1[B] ; ::_thesis: S1[B \/ {x}] consider X being Subset of T such that A6: ( X = union B & X is bounded ) by A5; reconsider x = x as Subset of T by A4; A7: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78 .= (union B) \/ x by ZFMISC_1:25 ; A8: x is bounded by A2, A4; ex Y being Subset of T st ( Y = union (B \/ {x}) & Y is bounded ) proof take X \/ x ; ::_thesis: ( X \/ x = union (B \/ {x}) & X \/ x is bounded ) thus ( X \/ x = union (B \/ {x}) & X \/ x is bounded ) by A6, A7, A8, Th13; ::_thesis: verum end; hence S1[B \/ {x}] ; ::_thesis: verum end; A9: S1[ {} ] proof set m = {} T; {} T = union {} by ZFMISC_1:2; hence S1[ {} ] ; ::_thesis: verum end; S1[Y] from FINSET_1:sch_2(A1, A9, A3); hence union Y is bounded ; ::_thesis: verum end; theorem Th18: :: TBSP_1:18 for N being non empty MetrStruct holds ( N is bounded iff [#] N is bounded ) proof let N be non empty MetrStruct ; ::_thesis: ( N is bounded iff [#] N is bounded ) thus ( N is bounded implies [#] N is bounded ) ::_thesis: ( [#] N is bounded implies N is bounded ) proof assume N is bounded ; ::_thesis: [#] N is bounded then consider r being Real such that A1: 0 < r and A2: for x, y being Point of N holds dist (x,y) <= r by Def6; for x, y being Point of N st x in [#] N & y in [#] N holds dist (x,y) <= r by A2; hence [#] N is bounded by A1, Def7; ::_thesis: verum end; assume [#] N is bounded ; ::_thesis: N is bounded then consider r being Real such that A3: 0 < r and A4: for x, y being Point of N st x in [#] N & y in [#] N holds dist (x,y) <= r by Def7; take r ; :: according to TBSP_1:def_6 ::_thesis: ( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) thus 0 < r by A3; ::_thesis: for x, y being Point of N holds dist (x,y) <= r let x, y be Point of N; ::_thesis: dist (x,y) <= r thus dist (x,y) <= r by A4; ::_thesis: verum end; registration let N be non empty bounded MetrStruct ; cluster [#] N -> bounded ; coherence [#] N is bounded by Th18; end; theorem :: TBSP_1:19 for T being non empty Reflexive symmetric triangle MetrStruct st T is totally_bounded holds T is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: ( T is totally_bounded implies T is bounded ) assume T is totally_bounded ; ::_thesis: T is bounded then consider Y being Subset-Family of T such that A1: ( Y is finite & the carrier of T = union Y ) and A2: for P being Subset of T st P in Y holds ex x being Element of T st P = Ball (x,1) by Def1; for P being Subset of T st P in Y holds P is bounded proof let P be Subset of T; ::_thesis: ( P in Y implies P is bounded ) assume P in Y ; ::_thesis: P is bounded then ex x being Element of T st P = Ball (x,1) by A2; hence P is bounded ; ::_thesis: verum end; then [#] T is bounded by A1, Th17; hence T is bounded by Th18; ::_thesis: verum end; definition let N be non empty Reflexive MetrStruct ; let C be Subset of N; assume A1: C is bounded ; func diameter C -> Real means :Def8: :: TBSP_1:def 8 ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= it ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds it <= s ) ) if C <> {} otherwise it = 0 ; consistency for b1 being Real holds verum ; existence ( ( C <> {} implies ex b1 being Real st ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds b1 <= s ) ) ) & ( not C <> {} implies ex b1 being Real st b1 = 0 ) ) proof thus ( C <> {} implies ex r being Real st ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r <= s ) ) ) ::_thesis: ( not C <> {} implies ex b1 being Real st b1 = 0 ) proof set c = the Element of C; defpred S1[ Real] means for x, y being Point of N st x in C & y in C holds dist (x,y) <= \$1; set I = { r where r is Real : S1[r] } ; defpred S2[ set ] means ex x, y being Point of N st ( x in C & y in C & \$1 = dist (x,y) ); set J = { r where r is Real : S2[r] } ; A2: for a, b being real number st a in { r where r is Real : S2[r] } & b in { r where r is Real : S1[r] } holds a <= b proof let a, b be real number ; ::_thesis: ( a in { r where r is Real : S2[r] } & b in { r where r is Real : S1[r] } implies a <= b ) assume ( a in { r where r is Real : S2[r] } & b in { r where r is Real : S1[r] } ) ; ::_thesis: a <= b then ( ex t being Real st ( t = a & ex x, y being Point of N st ( x in C & y in C & t = dist (x,y) ) ) & ex t9 being Real st ( t9 = b & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= t9 ) ) ) ; hence a <= b ; ::_thesis: verum end; A3: { r where r is Real : S2[r] } is Subset of REAL from DOMAIN_1:sch_7(); assume A4: C <> {} ; ::_thesis: ex r being Real st ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r <= s ) ) then reconsider c = the Element of C as Point of N by TARSKI:def_3; dist (c,c) = 0 by METRIC_1:1; then A5: 0 in { r where r is Real : S2[r] } by A4; reconsider J = { r where r is Real : S2[r] } as Subset of REAL by A3; A6: { r where r is Real : S1[r] } is Subset of REAL from DOMAIN_1:sch_7(); consider r being Real such that 0 < r and A7: for x, y being Point of N st x in C & y in C holds dist (x,y) <= r by A1, Def7; A8: r in { r where r is Real : S1[r] } by A7; reconsider I = { r where r is Real : S1[r] } as Subset of REAL by A6; consider d being real number such that A9: for a being real number st a in J holds a <= d and A10: for b being real number st b in I holds d <= b by A8, A5, A2, MEMBERED:37; take d ; ::_thesis: ( d is Real & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= d ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds d <= s ) ) thus d is Real by XREAL_0:def_1; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= d ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds d <= s ) ) thus for x, y being Point of N st x in C & y in C holds dist (x,y) <= d ::_thesis: for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds d <= s proof let x, y be Point of N; ::_thesis: ( x in C & y in C implies dist (x,y) <= d ) assume ( x in C & y in C ) ; ::_thesis: dist (x,y) <= d then dist (x,y) in J ; hence dist (x,y) <= d by A9; ::_thesis: verum end; let s be Real; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) implies d <= s ) assume for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ; ::_thesis: d <= s then s in I ; hence d <= s by A10; ::_thesis: verum end; thus ( not C <> {} implies ex b1 being Real st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real holds ( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds b1 <= s ) & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= b2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds b2 <= s ) implies b1 = b2 ) & ( not C <> {} & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let r1, r2 be Real; ::_thesis: ( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r2 <= s ) implies r1 = r2 ) & ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) ) hereby ::_thesis: ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) assume C <> {} ; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r2 <= s ) implies r1 = r2 ) assume ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds r2 <= s ) ) ; ::_thesis: r1 = r2 then ( r1 <= r2 & r2 <= r1 ) ; hence r1 = r2 by XXREAL_0:1; ::_thesis: verum end; thus ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) ; ::_thesis: verum end; end; :: deftheorem Def8 defines diameter TBSP_1:def_8_:_ for N being non empty Reflexive MetrStruct for C being Subset of N st C is bounded holds for b3 being Real holds ( ( C <> {} implies ( b3 = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= b3 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= s ) holds b3 <= s ) ) ) ) & ( not C <> {} implies ( b3 = diameter C iff b3 = 0 ) ) ); theorem :: TBSP_1:20 for T being non empty Reflexive symmetric triangle MetrStruct for x being set for P being Subset of T st P = {x} holds diameter P = 0 proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for x being set for P being Subset of T st P = {x} holds diameter P = 0 let x be set ; ::_thesis: for P being Subset of T st P = {x} holds diameter P = 0 let P be Subset of T; ::_thesis: ( P = {x} implies diameter P = 0 ) assume A1: P = {x} ; ::_thesis: diameter P = 0 then A2: x in P by TARSKI:def_1; then reconsider t1 = x as Element of T ; ( ( for x, y being Point of T st x in P & y in P holds dist (x,y) <= 0 ) & ( for s being Real st ( for x, y being Point of T st x in P & y in P holds dist (x,y) <= s ) holds 0 <= s ) ) proof thus for x, y being Point of T st x in P & y in P holds dist (x,y) <= 0 ::_thesis: for s being Real st ( for x, y being Point of T st x in P & y in P holds dist (x,y) <= s ) holds 0 <= s proof let x, y be Point of T; ::_thesis: ( x in P & y in P implies dist (x,y) <= 0 ) assume that A3: x in P and A4: y in P ; ::_thesis: dist (x,y) <= 0 x = t1 by A1, A3, TARSKI:def_1; then dist (x,y) = dist (t1,t1) by A1, A4, TARSKI:def_1 .= 0 by METRIC_1:1 ; hence dist (x,y) <= 0 ; ::_thesis: verum end; let s be Real; ::_thesis: ( ( for x, y being Point of T st x in P & y in P holds dist (x,y) <= s ) implies 0 <= s ) assume for x, y being Point of T st x in P & y in P holds dist (x,y) <= s ; ::_thesis: 0 <= s then dist (t1,t1) <= s by A2; hence 0 <= s by METRIC_1:1; ::_thesis: verum end; hence diameter P = 0 by A1, Def8; ::_thesis: verum end; theorem Th21: :: TBSP_1:21 for R being non empty Reflexive MetrStruct for S being Subset of R st S is bounded holds 0 <= diameter S proof let R be non empty Reflexive MetrStruct ; ::_thesis: for S being Subset of R st S is bounded holds 0 <= diameter S let S be Subset of R; ::_thesis: ( S is bounded implies 0 <= diameter S ) assume A1: S is bounded ; ::_thesis: 0 <= diameter S percases ( S = {} or S <> {} ) ; suppose S = {} ; ::_thesis: 0 <= diameter S hence 0 <= diameter S by Def8; ::_thesis: verum end; supposeA2: S <> {} ; ::_thesis: 0 <= diameter S set x = the Element of S; reconsider x = the Element of S as Element of R by A2, TARSKI:def_3; dist (x,x) <= diameter S by A1, A2, Def8; hence 0 <= diameter S by METRIC_1:1; ::_thesis: verum end; end; end; theorem :: TBSP_1:22 for M being non empty MetrSpace for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds ex g being Point of M st A = {g} proof let M be non empty MetrSpace; ::_thesis: for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds ex g being Point of M st A = {g} let A be Subset of M; ::_thesis: ( A <> {} & A is bounded & diameter A = 0 implies ex g being Point of M st A = {g} ) assume that A1: A <> {} and A2: A is bounded ; ::_thesis: ( not diameter A = 0 or ex g being Point of M st A = {g} ) thus ( diameter A = 0 implies ex g being Point of M st A = {g} ) ::_thesis: verum proof set g = the Element of A; reconsider g = the Element of A as Element of M by A1, TARSKI:def_3; assume A3: diameter A = 0 ; ::_thesis: ex g being Point of M st A = {g} reconsider Z = {g} as Subset of M ; take g ; ::_thesis: A = {g} for x being Element of M holds ( x in A iff x in Z ) proof let x be Element of M; ::_thesis: ( x in A iff x in Z ) thus ( x in A implies x in Z ) ::_thesis: ( x in Z implies x in A ) proof assume x in A ; ::_thesis: x in Z then dist (x,g) <= 0 by A2, A3, Def8; then dist (x,g) = 0 by METRIC_1:5; then x = g by METRIC_1:2; hence x in Z by TARSKI:def_1; ::_thesis: verum end; assume A4: x in Z ; ::_thesis: x in A g in A by A1; hence x in A by A4, TARSKI:def_1; ::_thesis: verum end; hence A = {g} by SUBSET_1:3; ::_thesis: verum end; end; theorem :: TBSP_1:23 for T being non empty Reflexive symmetric triangle MetrStruct for t1 being Element of T for r being Real st 0 < r holds diameter (Ball (t1,r)) <= 2 * r proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T for r being Real st 0 < r holds diameter (Ball (t1,r)) <= 2 * r let t1 be Element of T; ::_thesis: for r being Real st 0 < r holds diameter (Ball (t1,r)) <= 2 * r let r be Real; ::_thesis: ( 0 < r implies diameter (Ball (t1,r)) <= 2 * r ) A1: for x, y being Point of T st x in Ball (t1,r) & y in Ball (t1,r) holds dist (x,y) <= 2 * r proof let x, y be Point of T; ::_thesis: ( x in Ball (t1,r) & y in Ball (t1,r) implies dist (x,y) <= 2 * r ) assume ( x in Ball (t1,r) & y in Ball (t1,r) ) ; ::_thesis: dist (x,y) <= 2 * r then ( dist (t1,x) < r & dist (t1,y) < r ) by METRIC_1:11; then A2: (dist (t1,x)) + (dist (t1,y)) < r + r by XREAL_1:8; dist (x,y) <= (dist (x,t1)) + (dist (t1,y)) by METRIC_1:4; hence dist (x,y) <= 2 * r by A2, XXREAL_0:2; ::_thesis: verum end; assume 0 < r ; ::_thesis: diameter (Ball (t1,r)) <= 2 * r then t1 in Ball (t1,r) by Th11; hence diameter (Ball (t1,r)) <= 2 * r by A1, Def8; ::_thesis: verum end; theorem :: TBSP_1:24 for R being non empty Reflexive MetrStruct for S, V being Subset of R st S is bounded & V c= S holds diameter V <= diameter S proof let R be non empty Reflexive MetrStruct ; ::_thesis: for S, V being Subset of R st S is bounded & V c= S holds diameter V <= diameter S let S, V be Subset of R; ::_thesis: ( S is bounded & V c= S implies diameter V <= diameter S ) assume that A1: S is bounded and A2: V c= S ; ::_thesis: diameter V <= diameter S A3: V is bounded by A1, A2, Th14; percases ( V = {} or V <> {} ) ; suppose V = {} ; ::_thesis: diameter V <= diameter S then diameter V = 0 by Def8; hence diameter V <= diameter S by A1, Th21; ::_thesis: verum end; supposeA4: V <> {} ; ::_thesis: diameter V <= diameter S for x, y being Point of R st x in V & y in V holds dist (x,y) <= diameter S by A1, A2, Def8; hence diameter V <= diameter S by A3, A4, Def8; ::_thesis: verum end; end; end; theorem :: TBSP_1:25 for T being non empty Reflexive symmetric triangle MetrStruct for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds diameter (P \/ Q) <= (diameter P) + (diameter Q) proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds diameter (P \/ Q) <= (diameter P) + (diameter Q) let P, Q be Subset of T; ::_thesis: ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ Q) <= (diameter P) + (diameter Q) ) assume that A1: P is bounded and A2: Q is bounded and A3: P /\ Q <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: diameter (P \/ Q) <= (diameter P) + (diameter Q) set g = the Element of P /\ Q; A4: the Element of P /\ Q in Q by A3, XBOOLE_0:def_4; set s = (diameter P) + (diameter Q); set b = diameter Q; A5: diameter Q <= (diameter P) + (diameter Q) by A1, Th21, XREAL_1:31; set a = diameter P; A6: the Element of P /\ Q in P by A3, XBOOLE_0:def_4; reconsider g = the Element of P /\ Q as Element of T by A3, TARSKI:def_3; A7: diameter P <= (diameter P) + (diameter Q) by A2, Th21, XREAL_1:31; A8: for x, y being Point of T st x in P \/ Q & y in P \/ Q holds dist (x,y) <= (diameter P) + (diameter Q) proof let x, y be Point of T; ::_thesis: ( x in P \/ Q & y in P \/ Q implies dist (x,y) <= (diameter P) + (diameter Q) ) assume that A9: x in P \/ Q and A10: y in P \/ Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) A11: dist (x,y) <= (dist (x,g)) + (dist (g,y)) by METRIC_1:4; now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q) percases ( x in P or x in Q ) by A9, XBOOLE_0:def_3; supposeA12: x in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q) percases ( y in P or y in Q ) by A10, XBOOLE_0:def_3; suppose y in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) then dist (x,y) <= diameter P by A1, A12, Def8; hence dist (x,y) <= (diameter P) + (diameter Q) by A7, XXREAL_0:2; ::_thesis: verum end; supposeA13: y in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) A14: dist (x,g) <= diameter P by A1, A6, A12, Def8; dist (g,y) <= diameter Q by A2, A4, A13, Def8; then (dist (x,g)) + (dist (g,y)) <= (diameter P) + (diameter Q) by A14, XREAL_1:7; hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; ::_thesis: verum end; end; end; hence dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum end; supposeA15: x in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q) percases ( y in P or y in Q ) by A10, XBOOLE_0:def_3; supposeA16: y in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) A17: dist (x,g) <= diameter Q by A2, A4, A15, Def8; dist (g,y) <= diameter P by A1, A6, A16, Def8; then (dist (x,g)) + (dist (g,y)) <= (diameter Q) + (diameter P) by A17, XREAL_1:7; hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; ::_thesis: verum end; suppose y in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q) then dist (x,y) <= diameter Q by A2, A15, Def8; hence dist (x,y) <= (diameter P) + (diameter Q) by A5, XXREAL_0:2; ::_thesis: verum end; end; end; hence dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum end; end; end; hence dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum end; ( P <> {} & P \/ Q is bounded ) by A1, A2, A3, Th13; hence diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def8; ::_thesis: verum end; theorem :: TBSP_1:26 for T being non empty Reflexive symmetric triangle MetrStruct for S1 being sequence of T st S1 is Cauchy holds rng S1 is bounded proof let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for S1 being sequence of T st S1 is Cauchy holds rng S1 is bounded let S1 be sequence of T; ::_thesis: ( S1 is Cauchy implies rng S1 is bounded ) set A = rng S1; assume S1 is Cauchy ; ::_thesis: rng S1 is bounded then consider p being Element of NAT such that A1: for n, m being Element of NAT st p <= n & p <= m holds dist ((S1 . n),(S1 . m)) < 1 by Def4; defpred S1[ set ] means ex n being Element of NAT st ( p <= n & \$1 = S1 . n ); reconsider B = { t1 where t1 is Point of T : S1[t1] } as Subset of T from DOMAIN_1:sch_7(); defpred S2[ set ] means ex n being Element of NAT st ( n <= p & \$1 = S1 . n ); reconsider C = { t1 where t1 is Point of T : S2[t1] } as Subset of T from DOMAIN_1:sch_7(); reconsider B = B, C = C as Subset of T ; A2: C is finite proof set K = Seg p; set J = {0} \/ (Seg p); now__::_thesis:_for_x_being_set_holds_ (_(_x_in_C_implies_x_in_S1_.:_({0}_\/_(Seg_p))_)_&_(_x_in_S1_.:_({0}_\/_(Seg_p))_implies_x_in_C_)_) let x be set ; ::_thesis: ( ( x in C implies x in S1 .: ({0} \/ (Seg p)) ) & ( x in S1 .: ({0} \/ (Seg p)) implies x in C ) ) thus ( x in C implies x in S1 .: ({0} \/ (Seg p)) ) ::_thesis: ( x in S1 .: ({0} \/ (Seg p)) implies x in C ) proof assume x in C ; ::_thesis: x in S1 .: ({0} \/ (Seg p)) then consider t1 being Element of T such that A3: x = t1 and A4: ex n being Element of NAT st ( n <= p & t1 = S1 . n ) ; consider n being Element of NAT such that A5: n <= p and A6: t1 = S1 . n by A4; n in NAT ; then A7: n in dom S1 by FUNCT_2:def_1; now__::_thesis:_x_in_S1_.:_({0}_\/_(Seg_p)) percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: x in S1 .: ({0} \/ (Seg p)) then n in {0} by TARSKI:def_1; then n in {0} \/ (Seg p) by XBOOLE_0:def_3; hence x in S1 .: ({0} \/ (Seg p)) by A3, A6, A7, FUNCT_1:def_6; ::_thesis: verum end; suppose ex m being Nat st n = m + 1 ; ::_thesis: x in S1 .: ({0} \/ (Seg p)) then 1 <= n by NAT_1:11; then n in { k where k is Element of NAT : ( 1 <= k & k <= p ) } by A5; then n in Seg p by FINSEQ_1:def_1; then n in {0} \/ (Seg p) by XBOOLE_0:def_3; hence x in S1 .: ({0} \/ (Seg p)) by A3, A6, A7, FUNCT_1:def_6; ::_thesis: verum end; end; end; hence x in S1 .: ({0} \/ (Seg p)) ; ::_thesis: verum end; assume x in S1 .: ({0} \/ (Seg p)) ; ::_thesis: x in C then consider y being set such that A8: y in dom S1 and A9: y in {0} \/ (Seg p) and A10: x = S1 . y by FUNCT_1:def_6; reconsider y = y as Element of NAT by A8; now__::_thesis:_x_in_C percases ( y in {0} or y in Seg p ) by A9, XBOOLE_0:def_3; supposeA11: y in {0} ; ::_thesis: x in C S1 . y is Element of T ; then reconsider x9 = x as Element of T by A10; y = 0 by A11, TARSKI:def_1; then ex n being Element of NAT st ( n <= p & x9 = S1 . n ) by A10; hence x in C ; ::_thesis: verum end; supposeA12: y in Seg p ; ::_thesis: x in C S1 . y is Element of T ; then reconsider x9 = x as Element of T by A10; y in { k where k is Element of NAT : ( 1 <= k & k <= p ) } by A12, FINSEQ_1:def_1; then ex k being Element of NAT st ( y = k & 1 <= k & k <= p ) ; then ex n being Element of NAT st ( n <= p & x9 = S1 . n ) by A10; hence x in C ; ::_thesis: verum end; end; end; hence x in C ; ::_thesis: verum end; hence C is finite by TARSKI:1; ::_thesis: verum end; A13: rng S1 = B \/ C proof thus rng S1 c= B \/ C :: according to XBOOLE_0:def_10 ::_thesis: B \/ C c= rng S1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng S1 or x in B \/ C ) assume x in rng S1 ; ::_thesis: x in B \/ C then consider y being set such that A14: y in dom S1 and A15: x = S1 . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A14; S1 . y is Element of T ; then reconsider x9 = x as Element of T by A15; percases ( y <= p or p <= y ) ; suppose y <= p ; ::_thesis: x in B \/ C then ex n being Element of NAT st ( n <= p & x9 = S1 . n ) by A15; then x in C ; hence x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum end; suppose p <= y ; ::_thesis: x in B \/ C then ex n being Element of NAT st ( p <= n & x9 = S1 . n ) by A15; then x in B ; hence x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B \/ C or x in rng S1 ) assume A16: x in B \/ C ; ::_thesis: x in rng S1 percases ( x in B or x in C ) by A16, XBOOLE_0:def_3; suppose x in B ; ::_thesis: x in rng S1 then consider t1 being Element of T such that A17: x = t1 and A18: ex n being Element of NAT st ( p <= n & t1 = S1 . n ) ; consider n being Element of NAT such that p <= n and A19: t1 = S1 . n by A18; n in NAT ; then n in dom S1 by FUNCT_2:def_1; hence x in rng S1 by A17, A19, FUNCT_1:def_3; ::_thesis: verum end; suppose x in C ; ::_thesis: x in rng S1 then consider t1 being Element of T such that A20: x = t1 and A21: ex n being Element of NAT st ( n <= p & t1 = S1 . n ) ; consider n being Element of NAT such that n <= p and A22: t1 = S1 . n by A21; n in NAT ; then n in dom S1 by FUNCT_2:def_1; hence x in rng S1 by A20, A22, FUNCT_1:def_3; ::_thesis: verum end; end; end; B is bounded proof set x = S1 . p; ex r being Real ex t1 being Element of T st ( 0 < r & t1 in B & ( for z being Point of T st z in B holds dist (t1,z) <= r ) ) proof take 1 ; ::_thesis: ex t1 being Element of T st ( 0 < 1 & t1 in B & ( for z being Point of T st z in B holds dist (t1,z) <= 1 ) ) take S1 . p ; ::_thesis: ( 0 < 1 & S1 . p in B & ( for z being Point of T st z in B holds dist ((S1 . p),z) <= 1 ) ) thus 0 < 1 ; ::_thesis: ( S1 . p in B & ( for z being Point of T st z in B holds dist ((S1 . p),z) <= 1 ) ) thus S1 . p in B ; ::_thesis: for z being Point of T st z in B holds dist ((S1 . p),z) <= 1 let z be Point of T; ::_thesis: ( z in B implies dist ((S1 . p),z) <= 1 ) assume z in B ; ::_thesis: dist ((S1 . p),z) <= 1 then ex t1 being Element of T st ( z = t1 & ex n being Element of NAT st ( p <= n & t1 = S1 . n ) ) ; hence dist ((S1 . p),z) <= 1 by A1; ::_thesis: verum end; hence B is bounded by Th10; ::_thesis: verum end; hence rng S1 is bounded by A2, A13, Th13; ::_thesis: verum end;