:: FRECHET semantic presentation begin Lm1: for r being Real st r > 0 holds ex n being Element of NAT st ( 1 / n < r & n > 0 ) proof let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st ( 1 / n < r & n > 0 ) ) assume A1: r > 0 ; ::_thesis: ex n being Element of NAT st ( 1 / n < r & n > 0 ) consider n being Element of NAT such that A2: 1 / r < n by SEQ_4:3; take n ; ::_thesis: ( 1 / n < r & n > 0 ) 1 / (1 / r) > 1 / n by A1, A2, XREAL_1:88; hence 1 / n < r ; ::_thesis: n > 0 thus n > 0 by A1, A2; ::_thesis: verum end; theorem :: FRECHET:1 for T being non empty 1-sorted for S being sequence of T holds rng S is Subset of T ; theorem Th2: :: FRECHET:2 for T1 being non empty 1-sorted for T2 being 1-sorted for S being sequence of T1 st rng S c= the carrier of T2 holds S is sequence of T2 proof let T1 be non empty 1-sorted ; ::_thesis: for T2 being 1-sorted for S being sequence of T1 st rng S c= the carrier of T2 holds S is sequence of T2 let T2 be 1-sorted ; ::_thesis: for S being sequence of T1 st rng S c= the carrier of T2 holds S is sequence of T2 let S be sequence of T1; ::_thesis: ( rng S c= the carrier of T2 implies S is sequence of T2 ) A1: dom S = NAT by FUNCT_2:def_1; assume rng S c= the carrier of T2 ; ::_thesis: S is sequence of T2 hence S is sequence of T2 by A1, FUNCT_2:2; ::_thesis: verum end; theorem Th3: :: FRECHET:3 for T being non empty TopSpace for x being Point of T for B being Basis of x holds B <> {} proof let T be non empty TopSpace; ::_thesis: for x being Point of T for B being Basis of x holds B <> {} let x be Point of T; ::_thesis: for B being Basis of x holds B <> {} let B be Basis of x; ::_thesis: B <> {} A1: the carrier of T in the topology of T by PRE_TOPC:def_1; set U1 = [#] T; reconsider T = T as non empty TopStruct ; [#] T is open by A1, PRE_TOPC:def_2; then ex U2 being Subset of T st ( U2 in B & U2 c= [#] T ) by YELLOW_8:13; hence B <> {} ; ::_thesis: verum end; registration let T be non empty TopSpace; let x be Point of T; cluster open x -quasi_basis -> non empty for Element of K19(K19( the carrier of T)); coherence for b1 being Basis of x holds not b1 is empty by Th3; end; Lm2: for T being TopStruct for A being Subset of T holds ( A is open iff ([#] T) \ A is closed ) proof let T be TopStruct ; ::_thesis: for A being Subset of T holds ( A is open iff ([#] T) \ A is closed ) let A be Subset of T; ::_thesis: ( A is open iff ([#] T) \ A is closed ) thus ( A is open implies ([#] T) \ A is closed ) ::_thesis: ( ([#] T) \ A is closed implies A is open ) proof assume A is open ; ::_thesis: ([#] T) \ A is closed then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:3; hence ([#] T) \ A is closed by PRE_TOPC:def_3; ::_thesis: verum end; assume ([#] T) \ A is closed ; ::_thesis: A is open then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:def_3; hence A is open by PRE_TOPC:3; ::_thesis: verum end; theorem Th4: :: FRECHET:4 for T being TopSpace for A, B being Subset of T st A is open & B is closed holds A \ B is open proof let T be TopSpace; ::_thesis: for A, B being Subset of T st A is open & B is closed holds A \ B is open let A, B be Subset of T; ::_thesis: ( A is open & B is closed implies A \ B is open ) assume that A1: A is open and A2: B is closed ; ::_thesis: A \ B is open ([#] T) \ B is open by A2, PRE_TOPC:def_3; then A /\ (([#] T) \ B) is open by A1, TOPS_1:11; then A3: (A /\ ([#] T)) \ (A /\ B) is open by XBOOLE_1:50; A /\ ([#] T) = A by XBOOLE_1:28; hence A \ B is open by A3, XBOOLE_1:47; ::_thesis: verum end; theorem Th5: :: FRECHET:5 for T being TopStruct st {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds meet F is closed ) holds T is TopSpace proof let T be TopStruct ; ::_thesis: ( {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds meet F is closed ) implies T is TopSpace ) assume that A1: {} T is closed and A2: [#] T is closed and A3: for A, B being Subset of T st A is closed & B is closed holds A \/ B is closed and A4: for F being Subset-Family of T st F is closed holds meet F is closed ; ::_thesis: T is TopSpace A5: for A, B being Subset of T st A in the topology of T & B in the topology of T holds A /\ B in the topology of T proof let A, B be Subset of T; ::_thesis: ( A in the topology of T & B in the topology of T implies A /\ B in the topology of T ) assume that A6: A in the topology of T and A7: B in the topology of T ; ::_thesis: A /\ B in the topology of T reconsider A = A, B = B as Subset of T ; B is open by A7, PRE_TOPC:def_2; then A8: ([#] T) \ B is closed by Lm2; A is open by A6, PRE_TOPC:def_2; then ([#] T) \ A is closed by Lm2; then (([#] T) \ A) \/ (([#] T) \ B) is closed by A3, A8; then ([#] T) \ (A /\ B) is closed by XBOOLE_1:54; then A /\ B is open by Lm2; hence A /\ B in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; A9: for G being Subset-Family of T st G c= the topology of T holds union G in the topology of T proof let G be Subset-Family of T; ::_thesis: ( G c= the topology of T implies union G in the topology of T ) reconsider G9 = G as Subset-Family of T ; assume A10: G c= the topology of T ; ::_thesis: union G in the topology of T percases ( G = {} or G <> {} ) ; supposeA11: G = {} ; ::_thesis: union G in the topology of T ([#] T) \ ({} T) = [#] T ; then {} T is open by A2, Lm2; hence union G in the topology of T by A11, PRE_TOPC:def_2, ZFMISC_1:2; ::_thesis: verum end; supposeA12: G <> {} ; ::_thesis: union G in the topology of T reconsider CG = COMPLEMENT G as Subset-Family of T ; A13: for A being Subset of T st A in G holds ([#] T) \ A is closed proof let A be Subset of T; ::_thesis: ( A in G implies ([#] T) \ A is closed ) assume A in G ; ::_thesis: ([#] T) \ A is closed then A is open by A10, PRE_TOPC:def_2; hence ([#] T) \ A is closed by Lm2; ::_thesis: verum end; COMPLEMENT G is closed proof let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in COMPLEMENT G or A is closed ) assume A in COMPLEMENT G ; ::_thesis: A is closed then A ` in G9 by SETFAM_1:def_7; then ([#] T) \ (A `) is closed by A13; hence A is closed by PRE_TOPC:3; ::_thesis: verum end; then meet CG is closed by A4; then (union G9) ` is closed by A12, TOPS_2:6; then ([#] T) \ (union G) is closed ; then union G is open by Lm2; hence union G in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; end; end; ([#] T) \ ({} T) is open by A1, PRE_TOPC:def_3; then the carrier of T in the topology of T by PRE_TOPC:def_2; hence T is TopSpace by A9, A5, PRE_TOPC:def_1; ::_thesis: verum end; theorem Th6: :: FRECHET:6 for T being TopSpace for S being non empty TopStruct for f being Function of T,S st ( for A being Subset of S holds ( A is closed iff f " A is closed ) ) holds S is TopSpace proof let T be TopSpace; ::_thesis: for S being non empty TopStruct for f being Function of T,S st ( for A being Subset of S holds ( A is closed iff f " A is closed ) ) holds S is TopSpace let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st ( for A being Subset of S holds ( A is closed iff f " A is closed ) ) holds S is TopSpace let f be Function of T,S; ::_thesis: ( ( for A being Subset of S holds ( A is closed iff f " A is closed ) ) implies S is TopSpace ) assume A1: for A being Subset of S holds ( A is closed iff f " A is closed ) ; ::_thesis: S is TopSpace A2: for A, B being Subset of S st A is closed & B is closed holds A \/ B is closed proof let A, B be Subset of S; ::_thesis: ( A is closed & B is closed implies A \/ B is closed ) assume ( A is closed & B is closed ) ; ::_thesis: A \/ B is closed then ( f " A is closed & f " B is closed ) by A1; then (f " A) \/ (f " B) is closed by TOPS_1:9; then f " (A \/ B) is closed by RELAT_1:140; hence A \/ B is closed by A1; ::_thesis: verum end; ( {} T is closed & f " {} = {} ) ; then A3: {} S is closed by A1; A4: for F being Subset-Family of S st F is closed holds meet F is closed proof let F be Subset-Family of S; ::_thesis: ( F is closed implies meet F is closed ) assume A5: F is closed ; ::_thesis: meet F is closed percases ( F = {} S or F <> {} ) ; suppose F = {} S ; ::_thesis: meet F is closed hence meet F is closed by A3, SETFAM_1:def_1; ::_thesis: verum end; supposeA6: F <> {} ; ::_thesis: meet F is closed set F1 = { (f " A) where A is Subset of S : A in F } ; ex A being set st A in F proof set A = the Element of F; take the Element of F ; ::_thesis: the Element of F in F thus the Element of F in F by A6; ::_thesis: verum end; then consider A being Subset of S such that A7: A in F ; reconsider A = A as Subset of S ; A8: f " A in { (f " A) where A is Subset of S : A in F } by A7; { (f " A) where A is Subset of S : A in F } c= bool the carrier of T proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in { (f " A) where A is Subset of S : A in F } or B in bool the carrier of T ) assume B in { (f " A) where A is Subset of S : A in F } ; ::_thesis: B in bool the carrier of T then ex A being Subset of S st ( B = f " A & A in F ) ; hence B in bool the carrier of T ; ::_thesis: verum end; then reconsider F1 = { (f " A) where A is Subset of S : A in F } as Subset-Family of T ; A9: meet F1 c= f " (meet F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F1 or x in f " (meet F) ) assume A10: x in meet F1 ; ::_thesis: x in f " (meet F) for A being set st A in F holds f . x in A proof let A be set ; ::_thesis: ( A in F implies f . x in A ) assume A11: A in F ; ::_thesis: f . x in A then reconsider A = A as Subset of S ; f " A in F1 by A11; then x in f " A by A10, SETFAM_1:def_1; hence f . x in A by FUNCT_1:def_7; ::_thesis: verum end; then A12: f . x in meet F by A6, SETFAM_1:def_1; x in the carrier of T by A10; then x in dom f by FUNCT_2:def_1; hence x in f " (meet F) by A12, FUNCT_1:def_7; ::_thesis: verum end; F1 is closed proof let B be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not B in F1 or B is closed ) assume B in F1 ; ::_thesis: B is closed then consider A being Subset of S such that A13: f " A = B and A14: A in F ; A is closed by A5, A14, TOPS_2:def_2; hence B is closed by A1, A13; ::_thesis: verum end; then A15: meet F1 is closed by TOPS_2:22; f " (meet F) c= meet F1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (meet F) or x in meet F1 ) assume A16: x in f " (meet F) ; ::_thesis: x in meet F1 then A17: f . x in meet F by FUNCT_1:def_7; A18: x in dom f by A16, FUNCT_1:def_7; for B being set st B in F1 holds x in B proof let B be set ; ::_thesis: ( B in F1 implies x in B ) assume B in F1 ; ::_thesis: x in B then consider A being Subset of S such that A19: B = f " A and A20: A in F ; f . x in A by A17, A20, SETFAM_1:def_1; hence x in B by A18, A19, FUNCT_1:def_7; ::_thesis: verum end; hence x in meet F1 by A8, SETFAM_1:def_1; ::_thesis: verum end; then meet F1 = f " (meet F) by A9, XBOOLE_0:def_10; hence meet F is closed by A1, A15; ::_thesis: verum end; end; end; f " ([#] S) = [#] T by TOPS_2:41; then [#] S is closed by A1; hence S is TopSpace by A3, A2, A4, Th5; ::_thesis: verum end; theorem Th7: :: FRECHET:7 for x being Point of RealSpace for r being Real holds Ball (x,r) = ].(x - r),(x + r).[ proof let x be Point of RealSpace; ::_thesis: for r being Real holds Ball (x,r) = ].(x - r),(x + r).[ let r be Real; ::_thesis: Ball (x,r) = ].(x - r),(x + r).[ reconsider x2 = x as Real by METRIC_1:def_13; thus Ball (x,r) c= ].(x - r),(x + r).[ :: according to XBOOLE_0:def_10 ::_thesis: ].(x - r),(x + r).[ c= Ball (x,r) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (x,r) or y in ].(x - r),(x + r).[ ) assume A1: y in Ball (x,r) ; ::_thesis: y in ].(x - r),(x + r).[ then reconsider y1 = y as Element of RealSpace ; reconsider y2 = y1 as Element of REAL by METRIC_1:def_13; A2: dist (x,y1) = real_dist . (x2,y2) by METRIC_1:def_1, METRIC_1:def_13 .= abs (x2 - y2) by METRIC_1:def_12 .= abs (- (y2 - x2)) .= abs (y2 - x2) by COMPLEX1:52 ; dist (x,y1) < r by A1, METRIC_1:11; hence y in ].(x - r),(x + r).[ by A2, RCOMP_1:1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ].(x - r),(x + r).[ or y in Ball (x,r) ) assume A3: y in ].(x - r),(x + r).[ ; ::_thesis: y in Ball (x,r) then reconsider y2 = y as Real ; reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def_13; abs (y2 - x) = abs (- (y2 - x)) by COMPLEX1:52 .= abs (x - y2) .= real_dist . (x2,y2) by METRIC_1:def_12 ; then A4: real_dist . (x2,y2) < r by A3, RCOMP_1:1; dist (x1,y1) = real_dist . (x2,y2) by METRIC_1:def_1, METRIC_1:def_13; hence y in Ball (x,r) by A4, METRIC_1:11; ::_thesis: verum end; theorem :: FRECHET:8 for A being Subset of R^1 holds ( A is open iff for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ) proof let A be Subset of R^1; ::_thesis: ( A is open iff for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ) reconsider A1 = A as Subset of RealSpace by TOPMETR:12; thus ( A is open implies for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ) ::_thesis: ( ( for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ) implies A is open ) proof reconsider A1 = A as Subset of R^1 ; A1: the topology of R^1 = Family_open_set RealSpace by TOPMETR:12; assume A is open ; ::_thesis: for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) then A2: A1 in the topology of R^1 by PRE_TOPC:def_2; let x be Real; ::_thesis: ( x in A implies ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ) reconsider x1 = x as Element of REAL ; reconsider x1 = x1 as Element of RealSpace by METRIC_1:def_13; assume x in A ; ::_thesis: ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) then consider r being Real such that A3: r > 0 and A4: Ball (x1,r) c= A1 by A2, A1, PCOMPS_1:def_4; ].(x - r),(x + r).[ c= A1 by A4, Th7; hence ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) by A3; ::_thesis: verum end; assume A5: for x being Real st x in A holds ex r being Real st ( r > 0 & ].(x - r),(x + r).[ c= A ) ; ::_thesis: A is open for x being Element of RealSpace st x in A1 holds ex r being Real st ( r > 0 & Ball (x,r) c= A1 ) proof let x be Element of RealSpace; ::_thesis: ( x in A1 implies ex r being Real st ( r > 0 & Ball (x,r) c= A1 ) ) reconsider x1 = x as Real by METRIC_1:def_13; assume x in A1 ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= A1 ) then consider r being Real such that A6: r > 0 and A7: ].(x1 - r),(x1 + r).[ c= A1 by A5; Ball (x,r) c= A1 by A7, Th7; hence ex r being Real st ( r > 0 & Ball (x,r) c= A1 ) by A6; ::_thesis: verum end; then A8: A1 in Family_open_set RealSpace by PCOMPS_1:def_4; the topology of R^1 = Family_open_set RealSpace by TOPMETR:12; hence A is open by A8, PRE_TOPC:def_2; ::_thesis: verum end; theorem Th9: :: FRECHET:9 for S being sequence of R^1 st ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) holds rng S is closed proof let S be sequence of R^1; ::_thesis: ( ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) implies rng S is closed ) reconsider B = rng S as Subset of R^1 ; assume A1: for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ; ::_thesis: rng S is closed for x being Point of RealSpace st x in B ` holds ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) proof let x be Point of RealSpace; ::_thesis: ( x in B ` implies ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) ) assume A2: x in B ` ; ::_thesis: ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) reconsider x1 = x as Real by METRIC_1:def_13; percases ( ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B = {} or ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ) ; supposeA3: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B = {} ; ::_thesis: ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) reconsider C = Ball (x,(1 / 4)) as Subset of R^1 by TOPMETR:12; (Ball (x,(1 / 4))) /\ ((B `) `) = {} by A3, Th7; then C misses (B `) ` by XBOOLE_0:def_7; then Ball (x,(1 / 4)) c= B ` by SUBSET_1:24; hence ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) ; ::_thesis: verum end; supposeA4: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ; ::_thesis: ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) set y = the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B; A5: the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by A4, XBOOLE_0:def_4; A6: the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B in B by A4, XBOOLE_0:def_4; reconsider y = the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B as Real by A5; consider n1 being set such that A7: n1 in dom S and A8: y = S . n1 by A6, FUNCT_1:def_3; reconsider n1 = n1 as Element of NAT by A7; reconsider r = abs (x1 - y) as Real ; reconsider C = Ball (x,r) as Subset of R^1 by TOPMETR:12; abs (y - x1) < 1 / 4 by A5, RCOMP_1:1; then abs (- (x1 - y)) < 1 / 4 ; then A9: r <= 1 / 4 by COMPLEX1:52; Ball (x,r) misses rng S proof assume Ball (x,r) meets rng S ; ::_thesis: contradiction then consider z being set such that A10: z in Ball (x,r) and A11: z in rng S by XBOOLE_0:3; consider n2 being set such that A12: n2 in dom S and A13: z = S . n2 by A11, FUNCT_1:def_3; reconsider n2 = n2 as Element of NAT by A12; reconsider z = z as Real by A10, METRIC_1:def_13; percases ( n1 = n2 or n1 > n2 or n1 < n2 ) by XXREAL_0:1; supposeA14: n1 = n2 ; ::_thesis: contradiction A15: r = abs (0 + (- (y - x1))) .= abs (y - x1) by COMPLEX1:52 ; y in ].(x1 - r),(x1 + r).[ by A8, A10, A13, A14, Th7; hence contradiction by A15, RCOMP_1:1; ::_thesis: verum end; supposeA16: n1 > n2 ; ::_thesis: contradiction S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1; then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def_2; then ex a1 being Real st ( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ; then A17: n1 < y + (1 / 4) by A8, XREAL_1:19; S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1; then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def_2; then ex a2 being Real st ( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ; then z - (1 / 4) < n2 by A13, XREAL_1:19; then A18: n2 + 1 > (z - (1 / 4)) + 1 by XREAL_1:6; n2 + 1 <= n1 by A16, NAT_1:13; then n2 + 1 < y + (1 / 4) by A17, XXREAL_0:2; then z + ((- (1 / 4)) + 1) < y + (1 / 4) by A18, XXREAL_0:2; then A19: z < (y + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:20; Ball (x,r) c= Ball (x,(1 / 4)) by A9, PCOMPS_1:1; then z in Ball (x,(1 / 4)) by A10; then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7; then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def_2; then ex a1 being Real st ( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ; then A20: z + (1 / 4) > x1 by XREAL_1:19; y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def_2; then ex a1 being Real st ( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ; then y - (1 / 4) < (x1 + (1 / 4)) - (1 / 4) by XREAL_1:9; then z + (1 / 4) > y - (1 / 4) by A20, XXREAL_0:2; then (z + (1 / 4)) + (- (1 / 4)) > (y - (1 / 4)) + (- (1 / 4)) by XREAL_1:6; hence contradiction by A19; ::_thesis: verum end; supposeA21: n1 < n2 ; ::_thesis: contradiction S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1; then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def_2; then ex a2 being Real st ( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ; then A22: z + (1 / 4) > (n2 + (- (1 / 4))) + (1 / 4) by A13, XREAL_1:6; S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1; then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def_2; then ex a1 being Real st ( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ; then (n1 + (1 / 4)) - (1 / 4) > y - (1 / 4) by A8, XREAL_1:9; then A23: n1 + 1 > (y - (1 / 4)) + 1 by XREAL_1:6; n1 + 1 <= n2 by A21, NAT_1:13; then z + (1 / 4) > n1 + 1 by A22, XXREAL_0:2; then (y + (- (1 / 4))) + 1 < z + (1 / 4) by A23, XXREAL_0:2; then A24: (y + ((- (1 / 4)) + 1)) - ((- (1 / 4)) + 1) < (z + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:9; Ball (x,r) c= Ball (x,(1 / 4)) by A9, PCOMPS_1:1; then z in Ball (x,(1 / 4)) by A10; then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7; then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def_2; then ex a1 being Real st ( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ; then A25: z - (1 / 4) < x1 by XREAL_1:19; y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def_2; then ex a1 being Real st ( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ; then (x1 + (- (1 / 4))) + (1 / 4) < y + (1 / 4) by XREAL_1:6; then z - (1 / 4) < y + (1 / 4) by A25, XXREAL_0:2; then (z - (1 / 4)) + (1 / 4) < (y + (1 / 4)) + (1 / 4) by XREAL_1:6; then z - (1 / 2) < (y + (1 / 2)) - (1 / 2) by XREAL_1:9; hence contradiction by A24; ::_thesis: verum end; end; end; then C misses (B `) ` ; then A26: C c= B ` by SUBSET_1:24; x1 <> y proof assume x1 = y ; ::_thesis: contradiction then y in B /\ (B `) by A2, A6, XBOOLE_0:def_4; then B meets B ` by XBOOLE_0:4; hence contradiction by SUBSET_1:24; ::_thesis: verum end; then x1 + (- y) <> y + (- y) ; then abs (x1 - y) > 0 by COMPLEX1:47; hence ex r being real number st ( r > 0 & Ball (x,r) c= B ` ) by A26; ::_thesis: verum end; end; end; then ([#] R^1) \ (rng S) is open by TOPMETR:15; hence rng S is closed by PRE_TOPC:def_3; ::_thesis: verum end; theorem Th10: :: FRECHET:10 for B being Subset of R^1 st B = NAT holds B is closed proof let B be Subset of R^1; ::_thesis: ( B = NAT implies B is closed ) A1: dom (id NAT) = NAT ; A2: rng (id NAT) = NAT proof thus rng (id NAT) c= NAT ; :: according to XBOOLE_0:def_10 ::_thesis: NAT c= rng (id NAT) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in NAT or y in rng (id NAT) ) assume A3: y in NAT ; ::_thesis: y in rng (id NAT) thus y in rng (id NAT) by A3; ::_thesis: verum end; then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:2, TOPMETR:17; for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ proof let n be Element of NAT ; ::_thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ reconsider x = S . n as Real by FUNCT_1:17; A4: (- (1 / 4)) + n < 0 + n by XREAL_1:8; ( x = n & n < n + (1 / 4) ) by FUNCT_1:17, XREAL_1:29; then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A4; hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by RCOMP_1:def_2; ::_thesis: verum end; hence ( B = NAT implies B is closed ) by A2, Th9; ::_thesis: verum end; definition let M be non empty MetrStruct ; let x be Point of (TopSpaceMetr M); func Balls x -> Subset-Family of (TopSpaceMetr M) means :Def1: :: FRECHET:def 1 ex y being Point of M st ( y = x & it = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ); existence ex b1 being Subset-Family of (TopSpaceMetr M) ex y being Point of M st ( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) proof A1: the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12; then reconsider y = x as Point of M ; set B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ; { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } c= bool the carrier of (TopSpaceMetr M) proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } or A in bool the carrier of (TopSpaceMetr M) ) assume A in { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ; ::_thesis: A in bool the carrier of (TopSpaceMetr M) then ex n being Element of NAT st ( A = Ball (y,(1 / n)) & n <> 0 ) ; hence A in bool the carrier of (TopSpaceMetr M) by A1; ::_thesis: verum end; hence ex b1 being Subset-Family of (TopSpaceMetr M) ex y being Point of M st ( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of (TopSpaceMetr M) st ex y being Point of M st ( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) & ex y being Point of M st ( y = x & b2 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) holds b1 = b2 ; end; :: deftheorem Def1 defines Balls FRECHET:def_1_:_ for M being non empty MetrStruct for x being Point of (TopSpaceMetr M) for b3 being Subset-Family of (TopSpaceMetr M) holds ( b3 = Balls x iff ex y being Point of M st ( y = x & b3 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) ); registration let M be non empty MetrSpace; let x be Point of (TopSpaceMetr M); cluster Balls x -> open x -quasi_basis ; coherence ( Balls x is open & Balls x is x -quasi_basis ) proof set B = Balls x; consider x9 being Point of M such that A1: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1; A2: Balls x c= the topology of (TopSpaceMetr M) proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Balls x or A in the topology of (TopSpaceMetr M) ) assume A in Balls x ; ::_thesis: A in the topology of (TopSpaceMetr M) then consider n being Element of NAT such that A3: A = Ball (x9,(1 / n)) and n <> 0 by A1; Ball (x9,(1 / n)) in Family_open_set M by PCOMPS_1:29; hence A in the topology of (TopSpaceMetr M) by A3, TOPMETR:12; ::_thesis: verum end; A4: for O being set st O in Balls x holds x in O proof let O be set ; ::_thesis: ( O in Balls x implies x in O ) assume O in Balls x ; ::_thesis: x in O then ex n being Element of NAT st ( O = Ball (x9,(1 / n)) & n <> 0 ) by A1; hence x in O by A1, GOBOARD6:1; ::_thesis: verum end; A5: for O being Subset of (TopSpaceMetr M) st O is open & x in O holds ex V being Subset of (TopSpaceMetr M) st ( V in Balls x & V c= O ) proof let O be Subset of (TopSpaceMetr M); ::_thesis: ( O is open & x in O implies ex V being Subset of (TopSpaceMetr M) st ( V in Balls x & V c= O ) ) assume ( O is open & x in O ) ; ::_thesis: ex V being Subset of (TopSpaceMetr M) st ( V in Balls x & V c= O ) then consider r being real number such that A6: r > 0 and A7: Ball (x9,r) c= O by A1, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; consider n being Element of NAT such that A8: 1 / n < r and A9: n > 0 by A6, Lm1; reconsider Ba = Ball (x9,(1 / n)) as Subset of (TopSpaceMetr M) by TOPMETR:12; reconsider Ba = Ba as Subset of (TopSpaceMetr M) ; take Ba ; ::_thesis: ( Ba in Balls x & Ba c= O ) thus Ba in Balls x by A1, A9; ::_thesis: Ba c= O Ball (x9,(1 / n)) c= Ball (x9,r) by A8, PCOMPS_1:1; hence Ba c= O by A7, XBOOLE_1:1; ::_thesis: verum end; A10: Ball (x9,(1 / 1)) in Balls x by A1; then Intersect (Balls x) = meet (Balls x) by SETFAM_1:def_9; then x in Intersect (Balls x) by A10, A4, SETFAM_1:def_1; hence ( Balls x is open & Balls x is x -quasi_basis ) by A2, A5, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum end; end; registration let M be non empty MetrSpace; let x be Point of (TopSpaceMetr M); cluster Balls x -> countable ; coherence Balls x is countable proof set B = Balls x; consider x9 being Point of M such that A1: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1; deffunc H1( Element of NAT ) -> Element of K19( the carrier of M) = Ball (x9,(1 / M)); defpred S1[ Element of NAT ] means M <> 0 ; { H1(n) where n is Element of NAT : S1[n] } is countable from CARD_4:sch_1(); hence Balls x is countable by A1; ::_thesis: verum end; end; theorem Th11: :: FRECHET:11 for M being non empty MetrSpace for x being Point of (TopSpaceMetr M) for x9 being Point of M st x = x9 holds ex f being Function of NAT,(Balls x) st for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) proof let M be non empty MetrSpace; ::_thesis: for x being Point of (TopSpaceMetr M) for x9 being Point of M st x = x9 holds ex f being Function of NAT,(Balls x) st for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) let x be Point of (TopSpaceMetr M); ::_thesis: for x9 being Point of M st x = x9 holds ex f being Function of NAT,(Balls x) st for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) let x9 be Point of M; ::_thesis: ( x = x9 implies ex f being Function of NAT,(Balls x) st for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) ) assume A1: x = x9 ; ::_thesis: ex f being Function of NAT,(Balls x) st for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) set B = Balls x; consider x9 being Point of M such that A2: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1; defpred S1[ set , set ] means ex n9 being Element of NAT st ( $1 = n9 & $2 = Ball (x9,(1 / (n9 + 1))) ); A3: for n being set st n in NAT holds ex O being set st ( O in Balls x & S1[n,O] ) proof let n be set ; ::_thesis: ( n in NAT implies ex O being set st ( O in Balls x & S1[n,O] ) ) assume n in NAT ; ::_thesis: ex O being set st ( O in Balls x & S1[n,O] ) then reconsider n = n as Element of NAT ; take Ball (x9,(1 / (n + 1))) ; ::_thesis: ( Ball (x9,(1 / (n + 1))) in Balls x & S1[n, Ball (x9,(1 / (n + 1)))] ) thus ( Ball (x9,(1 / (n + 1))) in Balls x & S1[n, Ball (x9,(1 / (n + 1)))] ) by A2; ::_thesis: verum end; consider f being Function such that A4: ( dom f = NAT & rng f c= Balls x ) and A5: for n being set st n in NAT holds S1[n,f . n] from FUNCT_1:sch_5(A3); reconsider f = f as Function of NAT,(Balls x) by A4, FUNCT_2:2; take f ; ::_thesis: for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) let n be Element of NAT ; ::_thesis: f . n = Ball (x9,(1 / (n + 1))) S1[n,f . n] by A5; hence f . n = Ball (x9,(1 / (n + 1))) by A2, A1; ::_thesis: verum end; theorem Th12: :: FRECHET:12 for f, g being Function holds rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) proof let f, g be Function; ::_thesis: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) thus rng (f +* g) c= (f .: ((dom f) \ (dom g))) \/ (rng g) :: according to XBOOLE_0:def_10 ::_thesis: (f .: ((dom f) \ (dom g))) \/ (rng g) c= rng (f +* g) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f +* g) or y in (f .: ((dom f) \ (dom g))) \/ (rng g) ) assume y in rng (f +* g) ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g) then consider x being set such that A1: x in dom (f +* g) and A2: (f +* g) . x = y by FUNCT_1:def_3; percases ( x in dom g or not x in dom g ) ; supposeA3: x in dom g ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g) then y = g . x by A2, FUNCT_4:13; then y in rng g by A3, FUNCT_1:def_3; hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA4: not x in dom g ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g) x in (dom f) \/ (dom g) by A1, FUNCT_4:def_1; then x in dom f by A4, XBOOLE_0:def_3; then A5: x in (dom f) \ (dom g) by A4, XBOOLE_0:def_5; y = f . x by A2, A4, FUNCT_4:11; then y in f .: ((dom f) \ (dom g)) by A5, FUNCT_1:def_6; hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: ((dom f) \ (dom g))) \/ (rng g) or y in rng (f +* g) ) assume A6: y in (f .: ((dom f) \ (dom g))) \/ (rng g) ; ::_thesis: y in rng (f +* g) percases ( y in f .: ((dom f) \ (dom g)) or y in rng g ) by A6, XBOOLE_0:def_3; suppose y in f .: ((dom f) \ (dom g)) ; ::_thesis: y in rng (f +* g) then consider x being set such that A7: x in dom f and A8: x in (dom f) \ (dom g) and A9: f . x = y by FUNCT_1:def_6; not x in dom g by A8, XBOOLE_0:def_5; then A10: (f +* g) . x = f . x by FUNCT_4:11; x in (dom f) \/ (dom g) by A7, XBOOLE_0:def_3; then x in dom (f +* g) by FUNCT_4:def_1; hence y in rng (f +* g) by A9, A10, FUNCT_1:def_3; ::_thesis: verum end; supposeA11: y in rng g ; ::_thesis: y in rng (f +* g) rng g c= rng (f +* g) by FUNCT_4:18; hence y in rng (f +* g) by A11; ::_thesis: verum end; end; end; theorem Th13: :: FRECHET:13 for A, B being set st B c= A holds (id A) .: B = B proof let A, B be set ; ::_thesis: ( B c= A implies (id A) .: B = B ) assume A1: B c= A ; ::_thesis: (id A) .: B = B thus (id A) .: B c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= (id A) .: B proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (id A) .: B or y in B ) assume y in (id A) .: B ; ::_thesis: y in B then ex x being set st ( x in dom (id A) & x in B & (id A) . x = y ) by FUNCT_1:def_6; hence y in B by FUNCT_1:17; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in (id A) .: B ) assume A2: y in B ; ::_thesis: y in (id A) .: B then ( dom (id A) = A & (id A) . y = y ) by A1, FUNCT_1:17; hence y in (id A) .: B by A1, A2, FUNCT_1:def_6; ::_thesis: verum end; theorem Th14: :: FRECHET:14 for A, B, x being set holds dom ((id A) +* (B --> x)) = A \/ B proof let A, B, x be set ; ::_thesis: dom ((id A) +* (B --> x)) = A \/ B dom ((id A) +* (B --> x)) = (dom (id A)) \/ (dom (B --> x)) by FUNCT_4:def_1; then dom ((id A) +* (B --> x)) = A \/ (dom (B --> x)) ; hence dom ((id A) +* (B --> x)) = A \/ B by FUNCOP_1:13; ::_thesis: verum end; theorem Th15: :: FRECHET:15 for A, B, x being set st B <> {} holds rng ((id A) +* (B --> x)) = (A \ B) \/ {x} proof let A, B, x be set ; ::_thesis: ( B <> {} implies rng ((id A) +* (B --> x)) = (A \ B) \/ {x} ) set f = (id A) +* (B --> x); assume B <> {} ; ::_thesis: rng ((id A) +* (B --> x)) = (A \ B) \/ {x} then A1: rng (B --> x) = {x} by FUNCOP_1:8; thus rng ((id A) +* (B --> x)) c= (A \ B) \/ {x} :: according to XBOOLE_0:def_10 ::_thesis: (A \ B) \/ {x} c= rng ((id A) +* (B --> x)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((id A) +* (B --> x)) or y in (A \ B) \/ {x} ) assume y in rng ((id A) +* (B --> x)) ; ::_thesis: y in (A \ B) \/ {x} then consider x1 being set such that A2: x1 in dom ((id A) +* (B --> x)) and A3: y = ((id A) +* (B --> x)) . x1 by FUNCT_1:def_3; A4: x1 in (dom (id A)) \/ (dom (B --> x)) by A2, FUNCT_4:def_1; percases ( x1 in dom (B --> x) or not x1 in dom (B --> x) ) ; suppose x1 in dom (B --> x) ; ::_thesis: y in (A \ B) \/ {x} then ( ((id A) +* (B --> x)) . x1 = (B --> x) . x1 & (B --> x) . x1 = x ) by A4, FUNCOP_1:7, FUNCT_4:def_1; then y in {x} by A3, TARSKI:def_1; hence y in (A \ B) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; supposeA5: not x1 in dom (B --> x) ; ::_thesis: y in (A \ B) \/ {x} then A6: ((id A) +* (B --> x)) . x1 = (id A) . x1 by A4, FUNCT_4:def_1; A7: x1 in dom (id A) by A4, A5, XBOOLE_0:def_3; not x1 in B by A5, FUNCOP_1:13; then x1 in A \ B by A7, XBOOLE_0:def_5; then x1 in (A \ B) \/ {x} by XBOOLE_0:def_3; hence y in (A \ B) \/ {x} by A3, A6, A7, FUNCT_1:18; ::_thesis: verum end; end; end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (A \ B) \/ {x} or y in rng ((id A) +* (B --> x)) ) (id A) .: (A \ B) = A \ B by Th13; then (id A) .: ((dom (id A)) \ B) = A \ B ; then A8: (id A) .: ((dom (id A)) \ (dom (B --> x))) = A \ B by FUNCOP_1:13; assume y in (A \ B) \/ {x} ; ::_thesis: y in rng ((id A) +* (B --> x)) hence y in rng ((id A) +* (B --> x)) by A1, A8, Th12; ::_thesis: verum end; theorem Th16: :: FRECHET:16 for A, B, C, x being set st C c= A holds ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} proof let A, B, C, x be set ; ::_thesis: ( C c= A implies ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} ) assume A1: C c= A ; ::_thesis: ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} set f = (id A) +* (B --> x); thus ((id A) +* (B --> x)) " (C \ {x}) c= (C \ B) \ {x} :: according to XBOOLE_0:def_10 ::_thesis: (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x}) proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in ((id A) +* (B --> x)) " (C \ {x}) or x1 in (C \ B) \ {x} ) assume A2: x1 in ((id A) +* (B --> x)) " (C \ {x}) ; ::_thesis: x1 in (C \ B) \ {x} then A3: ((id A) +* (B --> x)) . x1 in C \ {x} by FUNCT_1:def_7; A4: not x1 in B proof assume A5: x1 in B ; ::_thesis: contradiction then A6: x1 in dom (B --> x) by FUNCOP_1:13; then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3; then ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A6, FUNCT_4:def_1; then A7: ((id A) +* (B --> x)) . x1 = x by A5, FUNCOP_1:7; not ((id A) +* (B --> x)) . x1 in {x} by A3, XBOOLE_0:def_5; hence contradiction by A7, TARSKI:def_1; ::_thesis: verum end; then A8: not x1 in dom (B --> x) ; x1 in dom ((id A) +* (B --> x)) by A2, FUNCT_1:def_7; then x1 in A \/ B by Th14; then A9: ( x1 in A or x1 in B ) by XBOOLE_0:def_3; then x1 in dom (id A) by A4; then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3; then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A8, FUNCT_4:def_1; then A10: ((id A) +* (B --> x)) . x1 = x1 by A4, A9, FUNCT_1:17; then A11: not x1 in {x} by A3, XBOOLE_0:def_5; x1 in C \ B by A3, A4, A10, XBOOLE_0:def_5; hence x1 in (C \ B) \ {x} by A11, XBOOLE_0:def_5; ::_thesis: verum end; let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) ) assume A12: x1 in (C \ B) \ {x} ; ::_thesis: x1 in ((id A) +* (B --> x)) " (C \ {x}) then not x1 in {x} by XBOOLE_0:def_5; then A13: x1 in C \ {x} by A12, XBOOLE_0:def_5; A14: x1 in C by A12; then x1 in A by A1; then x1 in dom (id A) ; then A15: x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3; x1 in C \ B by A12, XBOOLE_0:def_5; then not x1 in dom (B --> x) by XBOOLE_0:def_5; then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A15, FUNCT_4:def_1; then A16: ((id A) +* (B --> x)) . x1 = x1 by A1, A14, FUNCT_1:17; x1 in dom ((id A) +* (B --> x)) by A15, FUNCT_4:def_1; hence x1 in ((id A) +* (B --> x)) " (C \ {x}) by A13, A16, FUNCT_1:def_7; ::_thesis: verum end; theorem Th17: :: FRECHET:17 for A, B, x being set st not x in A holds ((id A) +* (B --> x)) " {x} = B proof let A, B, x be set ; ::_thesis: ( not x in A implies ((id A) +* (B --> x)) " {x} = B ) set f = (id A) +* (B --> x); assume A1: not x in A ; ::_thesis: ((id A) +* (B --> x)) " {x} = B thus ((id A) +* (B --> x)) " {x} c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= ((id A) +* (B --> x)) " {x} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((id A) +* (B --> x)) " {x} or y in B ) assume A2: y in ((id A) +* (B --> x)) " {x} ; ::_thesis: y in B then A3: y in dom ((id A) +* (B --> x)) by FUNCT_1:def_7; A4: ((id A) +* (B --> x)) . y in {x} by A2, FUNCT_1:def_7; percases ( y in dom (B --> x) or not y in dom (B --> x) ) ; suppose y in dom (B --> x) ; ::_thesis: y in B hence y in B ; ::_thesis: verum end; supposeA5: not y in dom (B --> x) ; ::_thesis: y in B then A6: ((id A) +* (B --> x)) . y = (id A) . y by FUNCT_4:11; A7: ( y in dom (B --> x) or y in dom (id A) ) by A3, FUNCT_4:12; then (id A) . y = y by A5, FUNCT_1:18; then y = x by A4, A6, TARSKI:def_1; hence y in B by A1, A7; ::_thesis: verum end; end; end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in ((id A) +* (B --> x)) " {x} ) assume A8: y in B ; ::_thesis: y in ((id A) +* (B --> x)) " {x} then A9: y in dom (B --> x) by FUNCOP_1:13; then ((id A) +* (B --> x)) . y = (B --> x) . y by FUNCT_4:13; then ((id A) +* (B --> x)) . y = x by A8, FUNCOP_1:7; then A10: ((id A) +* (B --> x)) . y in {x} by TARSKI:def_1; y in dom ((id A) +* (B --> x)) by A9, FUNCT_4:12; hence y in ((id A) +* (B --> x)) " {x} by A10, FUNCT_1:def_7; ::_thesis: verum end; theorem Th18: :: FRECHET:18 for A, B, C, x being set st C c= A & not x in A holds ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B proof let A, B, C, x be set ; ::_thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B ) assume that A1: C c= A and A2: not x in A ; ::_thesis: ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B A3: C \ {x} = C proof thus C \ {x} c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= C \ {x} let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C or y in C \ {x} ) assume A4: y in C ; ::_thesis: y in C \ {x} not y in {x} proof assume y in {x} ; ::_thesis: contradiction then y = x by TARSKI:def_1; hence contradiction by A1, A2, A4; ::_thesis: verum end; hence y in C \ {x} by A4, XBOOLE_0:def_5; ::_thesis: verum end; A5: ((C \ B) \ {x}) \/ B = C \/ B proof thus ((C \ B) \ {x}) \/ B c= C \/ B :: according to XBOOLE_0:def_10 ::_thesis: C \/ B c= ((C \ B) \ {x}) \/ B proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((C \ B) \ {x}) \/ B or y in C \/ B ) assume y in ((C \ B) \ {x}) \/ B ; ::_thesis: y in C \/ B then ( y in (C \ B) \ {x} or y in B ) by XBOOLE_0:def_3; hence y in C \/ B by XBOOLE_0:def_3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C \/ B or y in ((C \ B) \ {x}) \/ B ) assume y in C \/ B ; ::_thesis: y in ((C \ B) \ {x}) \/ B then A6: y in (C \ B) \/ B by XBOOLE_1:39; percases ( y in C \ B or y in B ) by A6, XBOOLE_0:def_3; supposeA7: y in C \ B ; ::_thesis: y in ((C \ B) \ {x}) \/ B then A8: y in C ; not y in {x} proof assume y in {x} ; ::_thesis: contradiction then x in C by A8, TARSKI:def_1; hence contradiction by A1, A2; ::_thesis: verum end; then y in (C \ B) \ {x} by A7, XBOOLE_0:def_5; hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def_3; ::_thesis: verum end; suppose y in B ; ::_thesis: y in ((C \ B) \ {x}) \/ B hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def_3; ::_thesis: verum end; end; end; set f = (id A) +* (B --> x); ((id A) +* (B --> x)) " {x} = B by A2, Th17; then ((id A) +* (B --> x)) " (C \/ {x}) = (((id A) +* (B --> x)) " C) \/ B by RELAT_1:140; hence ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B by A1, A3, A5, Th16; ::_thesis: verum end; theorem Th19: :: FRECHET:19 for A, B, C, x being set st C c= A & not x in A holds ((id A) +* (B --> x)) " (C \ {x}) = C \ B proof let A, B, C, x be set ; ::_thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \ {x}) = C \ B ) assume that A1: C c= A and A2: not x in A ; ::_thesis: ((id A) +* (B --> x)) " (C \ {x}) = C \ B not x in C \ B proof assume x in C \ B ; ::_thesis: contradiction then x in C ; hence contradiction by A1, A2; ::_thesis: verum end; then C \ B misses {x} by ZFMISC_1:50; then (C \ B) \ {x} = C \ B by XBOOLE_1:83; hence ((id A) +* (B --> x)) " (C \ {x}) = C \ B by A1, Th16; ::_thesis: verum end; begin definition let T be non empty TopStruct ; attrT is first-countable means :Def2: :: FRECHET:def 2 for x being Point of T ex B being Basis of x st B is countable ; end; :: deftheorem Def2 defines first-countable FRECHET:def_2_:_ for T being non empty TopStruct holds ( T is first-countable iff for x being Point of T ex B being Basis of x st B is countable ); theorem Th20: :: FRECHET:20 for M being non empty MetrSpace holds TopSpaceMetr M is first-countable proof let M be non empty MetrSpace; ::_thesis: TopSpaceMetr M is first-countable let x be Point of (TopSpaceMetr M); :: according to FRECHET:def_2 ::_thesis: ex B being Basis of x st B is countable take Balls x ; ::_thesis: Balls x is countable thus Balls x is countable ; ::_thesis: verum end; theorem :: FRECHET:21 R^1 is first-countable by Th20; registration cluster R^1 -> first-countable ; coherence R^1 is first-countable by Th20; end; definition let T be TopStruct ; let S be sequence of T; let x be Point of T; predS is_convergent_to x means :Def3: :: FRECHET:def 3 for U1 being Subset of T st U1 is open & x in U1 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1; end; :: deftheorem Def3 defines is_convergent_to FRECHET:def_3_:_ for T being TopStruct for S being sequence of T for x being Point of T holds ( S is_convergent_to x iff for U1 being Subset of T st U1 is open & x in U1 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 ); theorem Th22: :: FRECHET:22 for T being non empty TopStruct for x being Point of T for S being sequence of T st S = NAT --> x holds S is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: for x being Point of T for S being sequence of T st S = NAT --> x holds S is_convergent_to x let x be Point of T; ::_thesis: for S being sequence of T st S = NAT --> x holds S is_convergent_to x let S be sequence of T; ::_thesis: ( S = NAT --> x implies S is_convergent_to x ) assume A1: S = NAT --> x ; ::_thesis: S is_convergent_to x thus S is_convergent_to x ::_thesis: verum proof let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 ) assume that U1 is open and A2: x in U1 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 take 0 ; ::_thesis: for m being Element of NAT st 0 <= m holds S . m in U1 thus for m being Element of NAT st 0 <= m holds S . m in U1 by A1, A2, FUNCOP_1:7; ::_thesis: verum end; end; definition let T be TopStruct ; let S be sequence of T; attrS is convergent means :Def4: :: FRECHET:def 4 ex x being Point of T st S is_convergent_to x; end; :: deftheorem Def4 defines convergent FRECHET:def_4_:_ for T being TopStruct for S being sequence of T holds ( S is convergent iff ex x being Point of T st S is_convergent_to x ); definition let T be non empty TopStruct ; let S be sequence of T; func Lim S -> Subset of T means :Def5: :: FRECHET:def 5 for x being Point of T holds ( x in it iff S is_convergent_to x ); existence ex b1 being Subset of T st for x being Point of T holds ( x in b1 iff S is_convergent_to x ) proof defpred S1[ Element of T] means S is_convergent_to $1; { x where x is Element of T : S1[x] } is Subset of T from DOMAIN_1:sch_7(); then reconsider X = { x where x is Point of T : S1[x] } as Subset of T ; take X ; ::_thesis: for x being Point of T holds ( x in X iff S is_convergent_to x ) let y be Point of T; ::_thesis: ( y in X iff S is_convergent_to y ) ( y in X iff ex x being Point of T st ( x = y & S is_convergent_to x ) ) ; hence ( y in X iff S is_convergent_to y ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of T st ( for x being Point of T holds ( x in b1 iff S is_convergent_to x ) ) & ( for x being Point of T holds ( x in b2 iff S is_convergent_to x ) ) holds b1 = b2 proof let A, B be Subset of T; ::_thesis: ( ( for x being Point of T holds ( x in A iff S is_convergent_to x ) ) & ( for x being Point of T holds ( x in B iff S is_convergent_to x ) ) implies A = B ) assume that A1: for x being Point of T holds ( x in A iff S is_convergent_to x ) and A2: for x being Point of T holds ( x in B iff S is_convergent_to x ) ; ::_thesis: A = B for x being Point of T holds ( x in A iff x in B ) proof let x be Point of T; ::_thesis: ( x in A iff x in B ) ( x in A iff S is_convergent_to x ) by A1; hence ( x in A iff x in B ) by A2; ::_thesis: verum end; hence A = B by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def5 defines Lim FRECHET:def_5_:_ for T being non empty TopStruct for S being sequence of T for b3 being Subset of T holds ( b3 = Lim S iff for x being Point of T holds ( x in b3 iff S is_convergent_to x ) ); definition let T be non empty TopStruct ; attrT is Frechet means :Def6: :: FRECHET:def 6 for A being Subset of T for x being Point of T st x in Cl A holds ex S being sequence of T st ( rng S c= A & x in Lim S ); end; :: deftheorem Def6 defines Frechet FRECHET:def_6_:_ for T being non empty TopStruct holds ( T is Frechet iff for A being Subset of T for x being Point of T st x in Cl A holds ex S being sequence of T st ( rng S c= A & x in Lim S ) ); definition let T be non empty TopStruct ; attrT is sequential means :: FRECHET:def 7 for A being Subset of T holds ( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ); end; :: deftheorem defines sequential FRECHET:def_7_:_ for T being non empty TopStruct holds ( T is sequential iff for A being Subset of T holds ( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) ); theorem Th23: :: FRECHET:23 for T being non empty TopSpace st T is first-countable holds T is Frechet proof let T be non empty TopSpace; ::_thesis: ( T is first-countable implies T is Frechet ) assume A1: T is first-countable ; ::_thesis: T is Frechet let A be Subset of T; :: according to FRECHET:def_6 ::_thesis: for x being Point of T st x in Cl A holds ex S being sequence of T st ( rng S c= A & x in Lim S ) let x be Point of T; ::_thesis: ( x in Cl A implies ex S being sequence of T st ( rng S c= A & x in Lim S ) ) assume A2: x in Cl A ; ::_thesis: ex S being sequence of T st ( rng S c= A & x in Lim S ) consider B being Basis of x such that A3: B is countable by A1, Def2; consider f being Function of NAT,B such that A4: rng f = B by A3, CARD_3:96; defpred S1[ set , set ] means $2 in A /\ (meet (f .: (succ $1))); A5: for n being set st n in NAT holds ex y being set st ( y in the carrier of T & S1[n,y] ) proof defpred S2[ Element of NAT ] means ex H being Subset of T st ( H = meet (f .: (succ $1)) & H is open ); let n be set ; ::_thesis: ( n in NAT implies ex y being set st ( y in the carrier of T & S1[n,y] ) ) A6: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) given G being Subset of T such that A7: G = meet (f .: (succ n)) and A8: G is open ; ::_thesis: S2[n + 1] n + 1 in NAT ; then A9: n + 1 in dom f by FUNCT_2:def_1; ( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then A10: f . n in f .: (succ n) by FUNCT_1:def_6; f . (n + 1) in B ; then consider H1 being Subset of T such that A11: H1 = f . (n + 1) ; A12: H1 is open by A11, YELLOW_8:12; consider H being Subset of T such that A13: H = H1 /\ G ; take H ; ::_thesis: ( H = meet (f .: (succ (n + 1))) & H is open ) meet (f .: (succ (n + 1))) = meet (f .: ({(n + 1)} \/ (n + 1))) by ORDINAL1:def_1 .= meet (f .: ({(n + 1)} \/ (succ n))) by NAT_1:38 .= meet ((Im (f,(n + 1))) \/ (f .: (succ n))) by RELAT_1:120 .= meet ({(f . (n + 1))} \/ (f .: (succ n))) by A9, FUNCT_1:59 .= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by A10, SETFAM_1:9 .= H by A7, A11, A13, SETFAM_1:10 ; hence ( H = meet (f .: (succ (n + 1))) & H is open ) by A8, A12, A13, TOPS_1:11; ::_thesis: verum end; assume n in NAT ; ::_thesis: ex y being set st ( y in the carrier of T & S1[n,y] ) then reconsider n = n as Element of NAT ; A14: S2[ 0 ] proof f . 0 in B ; then reconsider H = f . 0 as Subset of T ; take H ; ::_thesis: ( H = meet (f .: (succ 0)) & H is open ) 0 in NAT ; then 0 in dom f by FUNCT_2:def_1; then meet (Im (f,0)) = meet {(f . 0)} by FUNCT_1:59 .= H by SETFAM_1:10 ; hence ( H = meet (f .: (succ 0)) & H is open ) by CARD_1:49, YELLOW_8:12; ::_thesis: verum end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A14, A6); then A15: ex H being Subset of T st ( H = meet (f .: (succ n)) & H is open ) ; A16: for G being set st G in f .: (succ n) holds x in G proof let G be set ; ::_thesis: ( G in f .: (succ n) implies x in G ) assume G in f .: (succ n) ; ::_thesis: x in G then consider k being set such that A17: k in dom f and k in succ n and A18: G = f . k by FUNCT_1:def_6; f . k in B by A17, FUNCT_2:5; hence x in G by A18, YELLOW_8:12; ::_thesis: verum end; ( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then f . n in f .: (succ n) by FUNCT_1:def_6; then x in meet (f .: (succ n)) by A16, SETFAM_1:def_1; then A meets meet (f .: (succ n)) by A2, A15, PRE_TOPC:def_7; then consider y being set such that A19: y in A /\ (meet (f .: (succ n))) by XBOOLE_0:4; take y ; ::_thesis: ( y in the carrier of T & S1[n,y] ) thus ( y in the carrier of T & S1[n,y] ) by A19; ::_thesis: verum end; consider S being Function such that A20: ( dom S = NAT & rng S c= the carrier of T & ( for n being set st n in NAT holds S1[n,S . n] ) ) from FUNCT_1:sch_5(A5); A21: rng S c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S or y in A ) assume y in rng S ; ::_thesis: y in A then consider a being set such that A22: ( a in dom S & y = S . a ) by FUNCT_1:def_3; y in A /\ (meet (f .: (succ a))) by A20, A22; hence y in A by XBOOLE_0:def_4; ::_thesis: verum end; reconsider S = S as sequence of T by A20, FUNCT_2:def_1, RELSET_1:4; A23: for m, n being Element of NAT st n <= m holds A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) proof let m, n be Element of NAT ; ::_thesis: ( n <= m implies A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) ) assume n <= m ; ::_thesis: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) then n + 1 <= m + 1 by XREAL_1:6; then n + 1 c= m + 1 by NAT_1:39; then succ n c= m + 1 by NAT_1:38; then succ n c= succ m by NAT_1:38; then A24: f .: (succ n) c= f .: (succ m) by RELAT_1:123; ( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then f . n in f .: (succ n) by FUNCT_1:def_6; then meet (f .: (succ m)) c= meet (f .: (succ n)) by A24, SETFAM_1:6; hence A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by XBOOLE_1:26; ::_thesis: verum end; S is_convergent_to x proof let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 ) assume A25: ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 reconsider U1 = U1 as Subset of T ; consider U2 being Subset of T such that A26: U2 in B and A27: U2 c= U1 by A25, YELLOW_8:13; consider n being set such that A28: n in dom f and A29: U2 = f . n by A4, A26, FUNCT_1:def_3; reconsider n = n as Element of NAT by A28; for m being Element of NAT st n <= m holds S . m in U1 proof let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in U1 ) ( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then A30: f . n in f .: (succ n) by FUNCT_1:def_6; assume n <= m ; ::_thesis: S . m in U1 then A31: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by A23; S . m in A /\ (meet (f .: (succ m))) by A20; then S . m in meet (f .: (succ n)) by A31, XBOOLE_0:def_4; then S . m in f . n by A30, SETFAM_1:def_1; hence S . m in U1 by A27, A29; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 ; ::_thesis: verum end; then x in Lim S by Def5; hence ex S being sequence of T st ( rng S c= A & x in Lim S ) by A21; ::_thesis: verum end; registration cluster non empty TopSpace-like first-countable -> non empty Frechet for TopStruct ; coherence for b1 being non empty TopSpace st b1 is first-countable holds b1 is Frechet by Th23; end; theorem Th24: :: FRECHET:24 for T being non empty TopSpace for A being Subset of T st A is closed holds for S being sequence of T st rng S c= A holds Lim S c= A proof let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is closed holds for S being sequence of T st rng S c= A holds Lim S c= A let A be Subset of T; ::_thesis: ( A is closed implies for S being sequence of T st rng S c= A holds Lim S c= A ) assume A1: A is closed ; ::_thesis: for S being sequence of T st rng S c= A holds Lim S c= A let S be sequence of T; ::_thesis: ( rng S c= A implies Lim S c= A ) assume A2: rng S c= A ; ::_thesis: Lim S c= A thus Lim S c= A ::_thesis: verum proof reconsider A = A as Subset of T ; reconsider L = Lim S as Subset of T ; L c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in L or y in A ) assume A3: y in L ; ::_thesis: y in A then reconsider p = y as Point of T ; A4: S is_convergent_to p by A3, Def5; for U1 being Subset of T st U1 is open & p in U1 holds A meets U1 proof let U1 be Subset of T; ::_thesis: ( U1 is open & p in U1 implies A meets U1 ) assume A5: U1 is open ; ::_thesis: ( not p in U1 or A meets U1 ) reconsider U2 = U1 as Subset of T ; assume p in U1 ; ::_thesis: A meets U1 then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds S . m in U2 by A4, A5, Def3; dom S = NAT by FUNCT_2:def_1; then A7: S . n in rng S by FUNCT_1:def_3; S . n in U1 by A6; then S . n in A /\ U1 by A2, A7, XBOOLE_0:def_4; hence A meets U1 by XBOOLE_0:def_7; ::_thesis: verum end; then p in Cl A by PRE_TOPC:def_7; hence y in A by A1, PRE_TOPC:22; ::_thesis: verum end; hence Lim S c= A ; ::_thesis: verum end; end; theorem Th25: :: FRECHET:25 for T being non empty TopSpace st ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) holds A is closed ) holds T is sequential proof let T be non empty TopSpace; ::_thesis: ( ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) holds A is closed ) implies T is sequential ) assume A1: for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) holds A is closed ; ::_thesis: T is sequential let A be Subset of T; :: according to FRECHET:def_7 ::_thesis: ( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) thus ( A is closed implies for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) by Th24; ::_thesis: ( ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) implies A is closed ) assume for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ; ::_thesis: A is closed hence A is closed by A1; ::_thesis: verum end; theorem Th26: :: FRECHET:26 for T being non empty TopSpace st T is Frechet holds T is sequential proof let T be non empty TopSpace; ::_thesis: ( T is Frechet implies T is sequential ) assume A1: T is Frechet ; ::_thesis: T is sequential for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) holds A is closed proof let A be Subset of T; ::_thesis: ( ( for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ) implies A is closed ) assume A2: for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A ; ::_thesis: A is closed A3: Cl A c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A ) assume A4: x in Cl A ; ::_thesis: x in A then reconsider p = x as Point of T ; consider S being sequence of T such that A5: rng S c= A and A6: p in Lim S by A1, A4, Def6; S is_convergent_to p by A6, Def5; then S is convergent by Def4; then Lim S c= A by A2, A5; hence x in A by A6; ::_thesis: verum end; A c= Cl A by PRE_TOPC:18; then A = Cl A by A3, XBOOLE_0:def_10; hence A is closed by PRE_TOPC:22; ::_thesis: verum end; hence T is sequential by Th25; ::_thesis: verum end; registration cluster non empty TopSpace-like Frechet -> non empty sequential for TopStruct ; coherence for b1 being non empty TopSpace st b1 is Frechet holds b1 is sequential by Th26; end; begin definition func REAL? -> non empty strict TopSpace means :Def8: :: FRECHET:def 8 ( the carrier of it = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,it st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of it holds ( A is closed iff f " A is closed ) ) ) ); existence ex b1 being non empty strict TopSpace st ( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds ( A is closed iff f " A is closed ) ) ) ) proof set f = (id REAL) +* (NAT --> REAL); reconsider X = (REAL \ NAT) \/ {REAL} as non empty set ; A1: rng ((id REAL) +* (NAT --> REAL)) c= (REAL \ NAT) \/ {REAL} by Th15; REAL \/ NAT = REAL by XBOOLE_1:12; then dom ((id REAL) +* (NAT --> REAL)) = the carrier of R^1 by Th14, TOPMETR:17; then reconsider f = (id REAL) +* (NAT --> REAL) as Function of the carrier of R^1,X by A1, FUNCT_2:2; set O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) } ; { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) } c= bool X proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) } or B in bool X ) assume B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) } ; ::_thesis: B in bool X then ex A being Subset of X st ( B = X \ A & ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) ) ; hence B in bool X ; ::_thesis: verum end; then reconsider O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st ( fA = f " A & fA is closed ) } as Subset-Family of X ; set T = TopStruct(# X,O #); reconsider f = f as Function of R^1,TopStruct(# X,O #) ; A2: for A being Subset of TopStruct(# X,O #) holds ( A is closed iff f " A is closed ) proof let A be Subset of TopStruct(# X,O #); ::_thesis: ( A is closed iff f " A is closed ) thus ( A is closed implies f " A is closed ) ::_thesis: ( f " A is closed implies A is closed ) proof assume A is closed ; ::_thesis: f " A is closed then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def_3; then ([#] TopStruct(# X,O #)) \ A in the topology of TopStruct(# X,O #) by PRE_TOPC:def_2; then consider B being Subset of X such that A3: X \ B = ([#] TopStruct(# X,O #)) \ A and A4: ex fA being Subset of R^1 st ( fA = f " B & fA is closed ) ; B = ([#] TopStruct(# X,O #)) \ (([#] TopStruct(# X,O #)) \ A) by A3, PRE_TOPC:3; hence f " A is closed by A4, PRE_TOPC:3; ::_thesis: verum end; assume f " A is closed ; ::_thesis: A is closed then X \ A in O ; then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def_2; hence A is closed by PRE_TOPC:def_3; ::_thesis: verum end; then reconsider T = TopStruct(# X,O #) as non empty strict TopSpace by Th6; take T ; ::_thesis: ( the carrier of T = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,T st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds ( A is closed iff f " A is closed ) ) ) ) thus the carrier of T = (REAL \ NAT) \/ {REAL} ; ::_thesis: ex f being Function of R^1,T st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds ( A is closed iff f " A is closed ) ) ) reconsider f = f as Function of R^1,T ; take f ; ::_thesis: ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds ( A is closed iff f " A is closed ) ) ) thus ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds ( A is closed iff f " A is closed ) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict TopSpace st the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds ( A is closed iff f " A is closed ) ) ) & the carrier of b2 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b2 st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b2 holds ( A is closed iff f " A is closed ) ) ) holds b1 = b2 proof let X, Y be non empty strict TopSpace; ::_thesis: ( the carrier of X = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,X st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of X holds ( A is closed iff f " A is closed ) ) ) & the carrier of Y = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,Y st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of Y holds ( A is closed iff f " A is closed ) ) ) implies X = Y ) assume that A5: the carrier of X = (REAL \ NAT) \/ {REAL} and A6: ex f being Function of R^1,X st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of X holds ( A is closed iff f " A is closed ) ) ) and A7: the carrier of Y = (REAL \ NAT) \/ {REAL} and A8: ex f being Function of R^1,Y st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of Y holds ( A is closed iff f " A is closed ) ) ) ; ::_thesis: X = Y consider g being Function of R^1,Y such that A9: g = (id REAL) +* (NAT --> REAL) and A10: for A being Subset of Y holds ( A is closed iff g " A is closed ) by A8; consider f being Function of R^1,X such that A11: f = (id REAL) +* (NAT --> REAL) and A12: for A being Subset of X holds ( A is closed iff f " A is closed ) by A6; A13: the topology of Y c= the topology of X proof let V be set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the topology of Y or V in the topology of X ) assume A14: V in the topology of Y ; ::_thesis: V in the topology of X then reconsider V1 = V as Subset of Y ; reconsider V2 = V as Subset of X by A5, A7, A14; reconsider V1 = V1 as Subset of Y ; reconsider V2 = V2 as Subset of X ; V1 is open by A14, PRE_TOPC:def_2; then ([#] Y) \ V1 is closed by Lm2; then f " (([#] Y) \ V1) is closed by A11, A9, A10; then ([#] X) \ V2 is closed by A5, A7, A12; then V2 is open by Lm2; hence V in the topology of X by PRE_TOPC:def_2; ::_thesis: verum end; the topology of X c= the topology of Y proof let V be set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the topology of X or V in the topology of Y ) assume A15: V in the topology of X ; ::_thesis: V in the topology of Y then reconsider V1 = V as Subset of X ; reconsider V2 = V as Subset of Y by A5, A7, A15; reconsider V1 = V1 as Subset of X ; reconsider V2 = V2 as Subset of Y ; V1 is open by A15, PRE_TOPC:def_2; then ([#] X) \ V1 is closed by Lm2; then g " (([#] X) \ V1) is closed by A11, A12, A9; then ([#] Y) \ V2 is closed by A5, A7, A10; then V2 is open by Lm2; hence V in the topology of Y by PRE_TOPC:def_2; ::_thesis: verum end; hence X = Y by A5, A7, A13, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def8 defines REAL? FRECHET:def_8_:_ for b1 being non empty strict TopSpace holds ( b1 = REAL? iff ( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds ( A is closed iff f " A is closed ) ) ) ) ); Lm3: {REAL} c= the carrier of REAL? proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {REAL} or x in the carrier of REAL? ) assume x in {REAL} ; ::_thesis: x in the carrier of REAL? then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3; hence x in the carrier of REAL? by Def8; ::_thesis: verum end; theorem Th27: :: FRECHET:27 REAL is Point of REAL? proof REAL in {REAL} by TARSKI:def_1; hence REAL is Point of REAL? by Lm3; ::_thesis: verum end; theorem Th28: :: FRECHET:28 for A being Subset of REAL? holds ( ( A is open & REAL in A ) iff ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) proof let A be Subset of REAL?; ::_thesis: ( ( A is open & REAL in A ) iff ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) consider f being Function of R^1,REAL? such that A1: f = (id REAL) +* (NAT --> REAL) and A2: for A being Subset of REAL? holds ( A is closed iff f " A is closed ) by Def8; thus ( A is open & REAL in A implies ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) ::_thesis: ( ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) implies ( A is open & REAL in A ) ) proof assume that A3: A is open and A4: REAL in A ; ::_thesis: ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) consider O being Subset of R^1 such that A5: O = (f " (A `)) ` ; A ` is closed by A3, TOPS_1:4; then f " (A `) is closed by A2; then A6: (f " (A `)) ` is open by TOPS_1:3; A7: not REAL in ([#] REAL?) \ A by A4, XBOOLE_0:def_5; A8: A ` c= (A `) \ {REAL} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ` or x in (A `) \ {REAL} ) assume A9: x in A ` ; ::_thesis: x in (A `) \ {REAL} then not x in {REAL} by A7, TARSKI:def_1; hence x in (A `) \ {REAL} by A9, XBOOLE_0:def_5; ::_thesis: verum end; A ` c= the carrier of REAL? ; then A10: A ` c= (REAL \ NAT) \/ {REAL} by Def8; A11: A ` c= REAL \ NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ` or x in REAL \ NAT ) assume A12: x in A ` ; ::_thesis: x in REAL \ NAT then ( x in REAL \ NAT or x in {REAL} ) by A10, XBOOLE_0:def_3; hence x in REAL \ NAT by A7, A12, TARSKI:def_1; ::_thesis: verum end; (A `) \ {REAL} c= A ` by XBOOLE_1:36; then A13: A ` = (A `) \ {REAL} by A8, XBOOLE_0:def_10; not REAL in REAL ; then ((id REAL) +* (NAT --> REAL)) " ((A `) \ {REAL}) = (A `) \ NAT by A11, Th19, XBOOLE_1:1; then O = (([#] R^1) \ (A `)) \/ (NAT /\ ([#] R^1)) by A1, A5, A13, XBOOLE_1:52; then A14: O = (([#] R^1) \ (A `)) \/ NAT by TOPMETR:17, XBOOLE_1:28; A = (A `) ` .= the carrier of REAL? \ (A `) ; then A15: A = ((REAL \ NAT) \/ {REAL}) \ (A `) by Def8; A16: A = ((REAL \ (A `)) \ NAT) \/ {REAL} proof thus A c= ((REAL \ (A `)) \ NAT) \/ {REAL} :: according to XBOOLE_0:def_10 ::_thesis: ((REAL \ (A `)) \ NAT) \/ {REAL} c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in ((REAL \ (A `)) \ NAT) \/ {REAL} ) assume A17: x in A ; ::_thesis: x in ((REAL \ (A `)) \ NAT) \/ {REAL} then A18: not x in A ` by XBOOLE_0:def_5; ( x in REAL \ NAT or x in {REAL} ) by A15, A17, XBOOLE_0:def_3; then ( ( x in REAL \ (A `) & not x in NAT ) or x in {REAL} ) by A18, XBOOLE_0:def_5; then ( x in (REAL \ (A `)) \ NAT or x in {REAL} ) by XBOOLE_0:def_5; hence x in ((REAL \ (A `)) \ NAT) \/ {REAL} by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((REAL \ (A `)) \ NAT) \/ {REAL} or x in A ) assume x in ((REAL \ (A `)) \ NAT) \/ {REAL} ; ::_thesis: x in A then ( x in (REAL \ (A `)) \ NAT or x in {REAL} ) by XBOOLE_0:def_3; then A19: ( ( x in REAL \ (A `) & not x in NAT ) or ( x in {REAL} & not x in A ` ) ) by A7, TARSKI:def_1, XBOOLE_0:def_5; then ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def_5; then A20: x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3; not x in A ` by A19, XBOOLE_0:def_5; hence x in A by A15, A20, XBOOLE_0:def_5; ::_thesis: verum end; NAT c= REAL \ (A `) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in REAL \ (A `) ) assume A21: x in NAT ; ::_thesis: x in REAL \ (A `) then not x in A ` by A11, XBOOLE_0:def_5; hence x in REAL \ (A `) by A21, XBOOLE_0:def_5; ::_thesis: verum end; then O = REAL \ (A `) by A14, TOPMETR:17, XBOOLE_1:12; hence ex O being Subset of R^1 st ( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) by A5, A6, A14, A16, XBOOLE_1:7; ::_thesis: verum end; given O being Subset of R^1 such that A22: O is open and A23: NAT c= O and A24: A = (O \ NAT) \/ {REAL} ; ::_thesis: ( A is open & REAL in A ) consider B being Subset of R^1 such that A25: B = ([#] R^1) \ O ; not REAL in REAL ; then ((id REAL) +* (NAT --> REAL)) " ((REAL \ O) \ {REAL}) = (REAL \ O) \ NAT by Th19; then A26: f " ((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1, XBOOLE_1:41; A27: B is closed by A22, A25, Lm2; A ` = ((REAL \ NAT) \/ {REAL}) \ ((O \ NAT) \/ {REAL}) by A24, Def8 .= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/ (O \ NAT))) by XBOOLE_1:42 .= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ {} by XBOOLE_1:46 .= ((REAL \ NAT) \ (O \ NAT)) \ {REAL} by XBOOLE_1:41 .= (REAL \ (NAT \/ (O \ NAT))) \ {REAL} by XBOOLE_1:41 .= (REAL \ (NAT \/ O)) \ {REAL} by XBOOLE_1:39 .= (REAL \ O) \ {REAL} by A23, XBOOLE_1:12 ; then f " (A `) = B by A23, A25, A26, TOPMETR:17, XBOOLE_1:12; then ([#] REAL?) \ A is closed by A2, A27; hence A is open by Lm2; ::_thesis: REAL in A REAL in {REAL} by TARSKI:def_1; hence REAL in A by A24, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th29: :: FRECHET:29 for A being set holds ( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) ) proof let A be set ; ::_thesis: ( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) ) thus ( A is Subset of REAL? & not REAL in A implies ( A is Subset of R^1 & NAT /\ A = {} ) ) ::_thesis: ( A is Subset of R^1 & NAT /\ A = {} implies ( A is Subset of REAL? & not REAL in A ) ) proof assume that A1: A is Subset of REAL? and A2: not REAL in A ; ::_thesis: ( A is Subset of R^1 & NAT /\ A = {} ) A c= the carrier of REAL? by A1; then A3: A c= (REAL \ NAT) \/ {REAL} by Def8; A c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in REAL ) assume A4: x in A ; ::_thesis: x in REAL then ( x in REAL \ NAT or x in {REAL} ) by A3, XBOOLE_0:def_3; hence x in REAL by A2, A4, TARSKI:def_1; ::_thesis: verum end; hence A is Subset of R^1 by TOPMETR:17; ::_thesis: NAT /\ A = {} thus NAT /\ A = {} ::_thesis: verum proof set x = the Element of NAT /\ A; assume A5: NAT /\ A <> {} ; ::_thesis: contradiction then A6: the Element of NAT /\ A in NAT by XBOOLE_0:def_4; A7: the Element of NAT /\ A in A by A5, XBOOLE_0:def_4; percases ( the Element of NAT /\ A in REAL \ NAT or the Element of NAT /\ A in {REAL} ) by A3, A7, XBOOLE_0:def_3; suppose the Element of NAT /\ A in REAL \ NAT ; ::_thesis: contradiction hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; suppose the Element of NAT /\ A in {REAL} ; ::_thesis: contradiction then the Element of NAT /\ A = REAL by TARSKI:def_1; then REAL in REAL by A6; hence contradiction ; ::_thesis: verum end; end; end; end; assume that A8: A is Subset of R^1 and A9: NAT /\ A = {} ; ::_thesis: ( A is Subset of REAL? & not REAL in A ) A10: A c= REAL \ NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in REAL \ NAT ) assume A11: x in A ; ::_thesis: x in REAL \ NAT then not x in NAT by A9, XBOOLE_0:def_4; hence x in REAL \ NAT by A8, A11, TOPMETR:17, XBOOLE_0:def_5; ::_thesis: verum end; REAL \ NAT c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:7; then A c= (REAL \ NAT) \/ {REAL} by A10, XBOOLE_1:1; hence A is Subset of REAL? by Def8; ::_thesis: not REAL in A thus not REAL in A ::_thesis: verum proof assume REAL in A ; ::_thesis: contradiction then REAL in REAL by A8, TOPMETR:17; hence contradiction ; ::_thesis: verum end; end; theorem Th30: :: FRECHET:30 for A being Subset of R^1 for B being Subset of REAL? st A = B holds ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) proof let A be Subset of R^1; ::_thesis: for B being Subset of REAL? st A = B holds ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) let B be Subset of REAL?; ::_thesis: ( A = B implies ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) ) consider f being Function of R^1,REAL? such that A1: f = (id REAL) +* (NAT --> REAL) and A2: for A being Subset of REAL? holds ( A is closed iff f " A is closed ) by Def8; assume A3: A = B ; ::_thesis: ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) A4: ( NAT /\ A = {} & not REAL in B implies f " (B `) = A ` ) proof assume that A5: NAT /\ A = {} and A6: not REAL in B ; ::_thesis: f " (B `) = A ` A7: REAL \ A = ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT proof thus REAL \ A c= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT :: according to XBOOLE_0:def_10 ::_thesis: ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT c= REAL \ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ A or x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT ) assume A8: x in REAL \ A ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT then A9: not x in A by XBOOLE_0:def_5; A10: x in REAL by A8; A11: not x in {REAL} proof assume x in {REAL} ; ::_thesis: contradiction then x = REAL by TARSKI:def_1; hence contradiction by A10; ::_thesis: verum end; percases ( x in NAT or not x in NAT ) ; suppose x in NAT ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT hence x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by XBOOLE_0:def_3; ::_thesis: verum end; suppose not x in NAT ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT then x in REAL \ NAT by A8, XBOOLE_0:def_5; then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3; then x in ((REAL \ NAT) \/ {REAL}) \ A by A9, XBOOLE_0:def_5; then x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} by A11, XBOOLE_0:def_5; hence x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT or x in REAL \ A ) assume A12: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT ; ::_thesis: x in REAL \ A percases ( x in NAT or x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} ) by A12, XBOOLE_0:def_3; supposeA13: x in NAT ; ::_thesis: x in REAL \ A then not x in A by A5, XBOOLE_0:def_4; hence x in REAL \ A by A13, XBOOLE_0:def_5; ::_thesis: verum end; supposeA14: x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} ; ::_thesis: x in REAL \ A then x in ((REAL \ NAT) \/ {REAL}) \ A by XBOOLE_0:def_5; then A15: not x in A by XBOOLE_0:def_5; ( x in REAL \ NAT or x in {REAL} ) by A14, XBOOLE_0:def_3; hence x in REAL \ A by A14, A15, XBOOLE_0:def_5; ::_thesis: verum end; end; end; B ` c= the carrier of REAL? ; then A16: B ` c= (REAL \ NAT) \/ {REAL} by Def8; A17: (B `) \ {REAL} c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B `) \ {REAL} or x in REAL ) assume A18: x in (B `) \ {REAL} ; ::_thesis: x in REAL then x in B ` by XBOOLE_0:def_5; then ( x in REAL \ NAT or x in {REAL} ) by A16, XBOOLE_0:def_3; hence x in REAL by A18, XBOOLE_0:def_5; ::_thesis: verum end; A19: REAL in ([#] REAL?) \ B by A6, Th27, XBOOLE_0:def_5; {REAL} c= B ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {REAL} or x in B ` ) assume x in {REAL} ; ::_thesis: x in B ` hence x in B ` by A19, TARSKI:def_1; ::_thesis: verum end; then ( not REAL in REAL & B ` = ((B `) \ {REAL}) \/ {REAL} ) by XBOOLE_1:45; then ((id REAL) +* (NAT --> REAL)) " (B `) = ((([#] REAL?) \ B) \ {REAL}) \/ NAT by A17, Th18 .= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by A3, Def8 ; hence f " (B `) = A ` by A1, A7, TOPMETR:17; ::_thesis: verum end; thus ( NAT /\ A = {} & A is open implies ( not REAL in B & B is open ) ) ::_thesis: ( not REAL in B & B is open implies ( NAT /\ A = {} & A is open ) ) proof assume that A20: NAT /\ A = {} and A21: A is open ; ::_thesis: ( not REAL in B & B is open ) thus not REAL in B by A3, A20, Th29; ::_thesis: B is open A ` is closed by A21, TOPS_1:4; then B ` is closed by A3, A2, A4, A20, Th29; hence B is open by TOPS_1:4; ::_thesis: verum end; assume that A22: not REAL in B and A23: B is open ; ::_thesis: ( NAT /\ A = {} & A is open ) thus NAT /\ A = {} by A3, A22, Th29; ::_thesis: A is open B ` is closed by A23, TOPS_1:4; then A ` is closed by A3, A2, A4, A22, Th29; hence A is open by TOPS_1:4; ::_thesis: verum end; theorem Th31: :: FRECHET:31 for A being Subset of REAL? st A = {REAL} holds A is closed proof reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:17; let A be Subset of REAL?; ::_thesis: ( A = {REAL} implies A is closed ) reconsider B = B as Subset of R^1 ; A1: REAL \ NAT = ((REAL \ NAT) \/ {REAL}) \ {REAL} proof thus REAL \ NAT c= ((REAL \ NAT) \/ {REAL}) \ {REAL} :: according to XBOOLE_0:def_10 ::_thesis: ((REAL \ NAT) \/ {REAL}) \ {REAL} c= REAL \ NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ NAT or x in ((REAL \ NAT) \/ {REAL}) \ {REAL} ) assume A2: x in REAL \ NAT ; ::_thesis: x in ((REAL \ NAT) \/ {REAL}) \ {REAL} then A3: x in REAL ; A4: not x in {REAL} proof assume x in {REAL} ; ::_thesis: contradiction then x = REAL by TARSKI:def_1; hence contradiction by A3; ::_thesis: verum end; x in (REAL \ NAT) \/ {REAL} by A2, XBOOLE_0:def_3; hence x in ((REAL \ NAT) \/ {REAL}) \ {REAL} by A4, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((REAL \ NAT) \/ {REAL}) \ {REAL} or x in REAL \ NAT ) assume A5: x in ((REAL \ NAT) \/ {REAL}) \ {REAL} ; ::_thesis: x in REAL \ NAT then not x in {REAL} by XBOOLE_0:def_5; hence x in REAL \ NAT by A5, XBOOLE_0:def_3; ::_thesis: verum end; B misses NAT by XBOOLE_1:79; then A6: B /\ NAT = {} by XBOOLE_0:def_7; then reconsider C = B as Subset of REAL? by Th29; assume A = {REAL} ; ::_thesis: A is closed then A7: C = A ` by A1, Def8; B is open proof reconsider N = NAT as Subset of R^1 by TOPMETR:17; reconsider N = N as Subset of R^1 ; ( N is closed & N ` = B ) by Th10, TOPMETR:17; hence B is open by TOPS_1:3; ::_thesis: verum end; then C is open by A6, Th30; hence A is closed by A7, TOPS_1:3; ::_thesis: verum end; theorem Th32: :: FRECHET:32 not REAL? is first-countable proof reconsider y = REAL as Point of REAL? by Th27; assume REAL? is first-countable ; ::_thesis: contradiction then consider B being Basis of y such that A1: B is countable by Def2; consider h being Function of NAT,B such that A2: rng h = B by A1, CARD_3:96; defpred S1[ set , set ] means ex m being Element of NAT st ( m = $1 & $2 in (h . $1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ); A3: for n being set st n in NAT holds ex x being set st ( x in REAL \ NAT & S1[n,x] ) proof let n be set ; ::_thesis: ( n in NAT implies ex x being set st ( x in REAL \ NAT & S1[n,x] ) ) assume A4: n in NAT ; ::_thesis: ex x being set st ( x in REAL \ NAT & S1[n,x] ) then reconsider m = n as Element of NAT ; n in dom h by A4, FUNCT_2:def_1; then A5: h . n in rng h by FUNCT_1:def_3; then reconsider Bn = h . n as Subset of REAL? by A2; reconsider m9 = m as Point of RealSpace by METRIC_1:def_13; reconsider Kn = Ball (m9,(1 / 4)) as Subset of R^1 by TOPMETR:12; reconsider Bn = Bn as Subset of REAL? ; ( Bn is open & y in Bn ) by A5, YELLOW_8:12; then consider An being Subset of R^1 such that A6: An is open and A7: NAT c= An and A8: Bn = (An \ NAT) \/ {REAL} by Th28; reconsider An9 = An as Subset of R^1 ; Kn is open by TOPMETR:14; then A9: An9 /\ Kn is open by A6, TOPS_1:11; dist (m9,m9) = 0 by METRIC_1:1; then m9 in Ball (m9,(1 / 4)) by METRIC_1:11; then n in An /\ (Ball (m9,(1 / 4))) by A4, A7, XBOOLE_0:def_4; then consider r being real number such that A10: r > 0 and A11: Ball (m9,r) c= An /\ Kn by A9, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; m < m + r by A10, XREAL_1:29; then m - r < m by XREAL_1:19; then consider x being real number such that A12: m - r < x and A13: x < m by XREAL_1:5; reconsider x = x as Real by XREAL_0:def_1; take x ; ::_thesis: ( x in REAL \ NAT & S1[n,x] ) A14: r < 1 proof assume r >= 1 ; ::_thesis: contradiction then 1 / 2 < r by XXREAL_0:2; then - r < - (1 / 2) by XREAL_1:24; then A15: (- r) + m < (- (1 / 2)) + m by XREAL_1:6; (- (1 / 2)) + m < r + m by A10, XREAL_1:6; then m - (1 / 2) in { a where a is Real : ( m - r < a & a < m + r ) } by A15; then m - (1 / 2) in ].(m - r),(m + r).[ by RCOMP_1:def_2; then m - (1 / 2) in Ball (m9,r) by Th7; then m - (1 / 2) in Kn by A11, XBOOLE_0:def_4; then m - (1 / 2) in ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7; then m - (1 / 2) in { a where a is Real : ( m - (1 / 4) < a & a < m + (1 / 4) ) } by RCOMP_1:def_2; then ex a being Real st ( a = m - (1 / 2) & m - (1 / 4) < a & a < m + (1 / 4) ) ; hence contradiction by XREAL_1:6; ::_thesis: verum end; A16: not x in NAT proof assume x in NAT ; ::_thesis: contradiction then reconsider x = x as Element of NAT ; percases ( x = m or x > m or x < m ) by XXREAL_0:1; suppose x = m ; ::_thesis: contradiction hence contradiction by A13; ::_thesis: verum end; suppose x > m ; ::_thesis: contradiction hence contradiction by A13; ::_thesis: verum end; supposeA17: x < m ; ::_thesis: contradiction m < x + r by A12, XREAL_1:19; then m - x < r by XREAL_1:19; then A18: m - x < 1 by A14, XXREAL_0:2; m >= x + 1 by A17, NAT_1:13; hence contradiction by A18, XREAL_1:19; ::_thesis: verum end; end; end; hence x in REAL \ NAT by XBOOLE_0:def_5; ::_thesis: S1[n,x] x + 0 < m + r by A10, A13, XREAL_1:8; then x in { a where a is Real : ( m - r < a & a < m + r ) } by A12; then x in ].(m - r),(m + r).[ by RCOMP_1:def_2; then A19: x in Ball (m9,r) by Th7; then x in An by A11, XBOOLE_0:def_4; then x in An \ NAT by A16, XBOOLE_0:def_5; then A20: x in Bn by A8, XBOOLE_0:def_3; take m ; ::_thesis: ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) Ball (m9,(1 / 4)) = ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7; then x in ].(m - (1 / 4)),(m + (1 / 4)).[ by A11, A19, XBOOLE_0:def_4; hence ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A20, XBOOLE_0:def_4; ::_thesis: verum end; consider S being Function such that A21: dom S = NAT and A22: rng S c= REAL \ NAT and A23: for n being set st n in NAT holds S1[n,S . n] from FUNCT_1:sch_5(A3); reconsider S = S as sequence of R^1 by A21, A22, FUNCT_2:2, TOPMETR:17, XBOOLE_1:1; reconsider O = rng S as Subset of R^1 ; for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ proof let n be Element of NAT ; ::_thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ex m being Element of NAT st ( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23; hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by XBOOLE_0:def_4; ::_thesis: verum end; then O is closed by Th9; then A24: ([#] R^1) \ O is open by PRE_TOPC:def_3; set A = ((O `) \ NAT) \/ {REAL}; ((O `) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((O `) \ NAT) \/ {REAL} or x in (REAL \ NAT) \/ {REAL} ) assume x in ((O `) \ NAT) \/ {REAL} ; ::_thesis: x in (REAL \ NAT) \/ {REAL} then ( x in (O `) \ NAT or x in {REAL} ) by XBOOLE_0:def_3; then ( ( x in O ` & not x in NAT ) or x in {REAL} ) by XBOOLE_0:def_5; then ( x in REAL \ NAT or x in {REAL} ) by TOPMETR:17, XBOOLE_0:def_5; hence x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3; ::_thesis: verum end; then reconsider A = ((O `) \ NAT) \/ {REAL} as Subset of REAL? by Def8; reconsider A = A as Subset of REAL? ; NAT c= O ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in O ` ) assume A25: x in NAT ; ::_thesis: x in O ` then not x in rng S by A22, XBOOLE_0:def_5; hence x in O ` by A25, TOPMETR:17, XBOOLE_0:def_5; ::_thesis: verum end; then ( A is open & REAL in A ) by A24, Th28; then consider V being Subset of REAL? such that A26: V in B and A27: V c= A by YELLOW_8:13; consider n1 being set such that A28: n1 in dom h and A29: V = h . n1 by A2, A26, FUNCT_1:def_3; reconsider n = n1 as Element of NAT by A28; for n being Element of NAT ex x being set st ( x in h . n & not x in A ) proof let n be Element of NAT ; ::_thesis: ex x being set st ( x in h . n & not x in A ) consider xn being set such that A30: xn = S . n ; take xn ; ::_thesis: ( xn in h . n & not xn in A ) A31: S . n in rng S by A21, FUNCT_1:def_3; then not xn in ([#] R^1) \ O by A30, XBOOLE_0:def_5; then A32: not xn in (O `) \ NAT by XBOOLE_0:def_5; not xn = REAL proof assume xn = REAL ; ::_thesis: contradiction then REAL in REAL by A22, A30, A31, XBOOLE_0:def_5; hence contradiction ; ::_thesis: verum end; then A33: not xn in {REAL} by TARSKI:def_1; ex m being Element of NAT st ( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23; hence ( xn in h . n & not xn in A ) by A30, A32, A33, XBOOLE_0:def_3, XBOOLE_0:def_4; ::_thesis: verum end; then ex x being set st ( x in h . n & not x in A ) ; hence contradiction by A27, A29; ::_thesis: verum end; theorem Th33: :: FRECHET:33 REAL? is Frechet proof let A be Subset of REAL?; :: according to FRECHET:def_6 ::_thesis: for x being Point of REAL? st x in Cl A holds ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) let x be Point of REAL?; ::_thesis: ( x in Cl A implies ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) ) assume A1: x in Cl A ; ::_thesis: ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) x in the carrier of REAL? ; then x in (REAL \ NAT) \/ {REAL} by Def8; then A2: ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def_3; percases ( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) ) by A2, TARSKI:def_1; supposeA3: x in REAL \ NAT ; ::_thesis: ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) then A4: x in REAL ; A c= the carrier of REAL? ; then A5: A c= (REAL \ NAT) \/ {REAL} by Def8; A \ {REAL} c= REAL proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A \ {REAL} or a in REAL ) assume A6: a in A \ {REAL} ; ::_thesis: a in REAL then a in A by XBOOLE_0:def_5; then ( a in REAL \ NAT or a in {REAL} ) by A5, XBOOLE_0:def_3; hence a in REAL by A6, XBOOLE_0:def_5; ::_thesis: verum end; then reconsider A9 = A \ {REAL} as Subset of R^1 by TOPMETR:17; reconsider x9 = x as Point of R^1 by A3, TOPMETR:17; reconsider A9 = A9 as Subset of R^1 ; for B9 being Subset of R^1 st B9 is open & x9 in B9 holds A9 meets B9 proof reconsider C = NAT as Subset of R^1 by TOPMETR:17; let B9 be Subset of R^1; ::_thesis: ( B9 is open & x9 in B9 implies A9 meets B9 ) reconsider B1 = B9 as Subset of R^1 ; reconsider C = C as Subset of R^1 ; A7: not x9 in NAT by A3, XBOOLE_0:def_5; B9 \ NAT misses NAT by XBOOLE_1:79; then A8: (B9 \ NAT) /\ NAT = {} by XBOOLE_0:def_7; then reconsider D = B1 \ C as Subset of REAL? by Th29; assume B9 is open ; ::_thesis: ( not x9 in B9 or A9 meets B9 ) then B1 \ C is open by Th4, Th10; then A9: D is open by A8, Th30; reconsider D = D as Subset of REAL? ; assume x9 in B9 ; ::_thesis: A9 meets B9 then x9 in B9 \ NAT by A7, XBOOLE_0:def_5; then A meets D by A1, A9, PRE_TOPC:def_7; then A10: A /\ D <> {} by XBOOLE_0:def_7; A9 /\ B9 <> {} proof set a = the Element of A /\ D; A11: the Element of A /\ D in D by A10, XBOOLE_0:def_4; then A12: the Element of A /\ D in B9 by XBOOLE_0:def_5; A13: the Element of A /\ D in REAL by A11, TOPMETR:17; A14: not the Element of A /\ D in {REAL} proof assume the Element of A /\ D in {REAL} ; ::_thesis: contradiction then the Element of A /\ D = REAL by TARSKI:def_1; hence contradiction by A13; ::_thesis: verum end; the Element of A /\ D in A by A10, XBOOLE_0:def_4; then the Element of A /\ D in A \ {REAL} by A14, XBOOLE_0:def_5; hence A9 /\ B9 <> {} by A12, XBOOLE_0:def_4; ::_thesis: verum end; hence A9 meets B9 by XBOOLE_0:def_7; ::_thesis: verum end; then x9 in Cl A9 by PRE_TOPC:def_7; then consider S9 being sequence of R^1 such that A15: rng S9 c= A9 and A16: x9 in Lim S9 by Def6; A17: rng S9 c= A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng S9 or a in A ) assume a in rng S9 ; ::_thesis: a in A hence a in A by A15, XBOOLE_0:def_5; ::_thesis: verum end; then reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1:1; take S ; ::_thesis: ( rng S c= A & x in Lim S ) thus rng S c= A by A17; ::_thesis: x in Lim S A18: S9 is_convergent_to x9 by A16, Def5; S is_convergent_to x proof reconsider C = {REAL} as Subset of REAL? by Lm3; let V be Subset of REAL?; :: according to FRECHET:def_3 ::_thesis: ( V is open & x in V implies ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in V ) assume that A19: V is open and A20: x in V ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in V reconsider C = C as Subset of REAL? ; REAL in {REAL} by TARSKI:def_1; then A21: not REAL in V \ {REAL} by XBOOLE_0:def_5; then reconsider V9 = V \ C as Subset of R^1 by Th29; V \ C is open by A19, Th4, Th31; then A22: V9 is open by A21, Th30; not x in C proof assume x in C ; ::_thesis: contradiction then x = REAL by TARSKI:def_1; hence contradiction by A4; ::_thesis: verum end; then x in V \ C by A20, XBOOLE_0:def_5; then consider n being Element of NAT such that A23: for m being Element of NAT st n <= m holds S9 . m in V9 by A18, A22, Def3; take n ; ::_thesis: for m being Element of NAT st n <= m holds S . m in V thus for m being Element of NAT st n <= m holds S . m in V ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in V ) assume n <= m ; ::_thesis: S . m in V then S9 . m in V9 by A23; hence S . m in V by XBOOLE_0:def_5; ::_thesis: verum end; end; hence x in Lim S by Def5; ::_thesis: verum end; supposeA24: ( x = REAL & x in A ) ; ::_thesis: ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) reconsider S = NAT --> x as sequence of REAL? ; take S ; ::_thesis: ( rng S c= A & x in Lim S ) {x} c= A by A24, ZFMISC_1:31; hence rng S c= A by FUNCOP_1:8; ::_thesis: x in Lim S S is_convergent_to x by Th22; hence x in Lim S by Def5; ::_thesis: verum end; supposeA25: ( x = REAL & not x in A ) ; ::_thesis: ex S being sequence of REAL? st ( rng S c= A & x in Lim S ) then reconsider A9 = A as Subset of R^1 by Th29; ex k being Point of R^1 st ( k in NAT & ex S9 being sequence of R^1 st ( rng S9 c= A9 & S9 is_convergent_to k ) ) proof defpred S1[ set , set ] means ( $1 in $2 & $2 in the topology of R^1 & $2 /\ A9 = {} ); assume A26: for k being Point of R^1 holds ( not k in NAT or for S9 being sequence of R^1 holds ( not rng S9 c= A9 or not S9 is_convergent_to k ) ) ; ::_thesis: contradiction A27: for k being set st k in NAT holds ex U1 being set st S1[k,U1] proof given k being set such that A28: k in NAT and A29: for U1 being set st k in U1 & U1 in the topology of R^1 holds not U1 /\ A9 = {} ; ::_thesis: contradiction reconsider k = k as Point of R^1 by A28, TOPMETR:17; reconsider k99 = k as Point of (TopSpaceMetr RealSpace) ; reconsider k9 = k99 as Point of RealSpace by TOPMETR:12; set Bs = Balls k99; consider h being Function of NAT,(Balls k99) such that A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11; defpred S2[ set , set ] means $2 in (h . $1) /\ A9; A31: for n being set st n in NAT holds ex z being set st ( z in the carrier of R^1 & S2[n,z] ) proof let n be set ; ::_thesis: ( n in NAT implies ex z being set st ( z in the carrier of R^1 & S2[n,z] ) ) assume n in NAT ; ::_thesis: ex z being set st ( z in the carrier of R^1 & S2[n,z] ) then reconsider n = n as Element of NAT ; A32: h . n in Balls k99 ; then reconsider H = h . n as Subset of R^1 ; take z = the Element of H /\ A9; ::_thesis: ( z in the carrier of R^1 & S2[n,z] ) Balls k99 c= the topology of R^1 by TOPS_2:64; then A33: H /\ A9 <> {} by A29, A32, YELLOW_8:12; then z in H by XBOOLE_0:def_4; hence ( z in the carrier of R^1 & S2[n,z] ) by A33; ::_thesis: verum end; consider S9 being Function such that A34: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and A35: for n being set st n in NAT holds S2[n,S9 . n] from FUNCT_1:sch_5(A31); reconsider S9 = S9 as Function of NAT, the carrier of R^1 by A34, FUNCT_2:2; A36: S9 is_convergent_to k proof let U1 be Subset of R^1; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & k in U1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds S9 . m in U1 ) assume ( U1 is open & k in U1 ) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds S9 . m in U1 then consider r being real number such that A37: r > 0 and A38: Ball (k9,r) c= U1 by TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; consider n being Element of NAT such that A39: 1 / n < r and A40: n > 0 by A37, Lm1; take n ; ::_thesis: for m being Element of NAT st n <= m holds S9 . m in U1 thus for m being Element of NAT st n <= m holds S9 . m in U1 ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ( n <= m implies S9 . m in U1 ) S9 . m in (h . m) /\ A9 by A35; then A41: S9 . m in h . m by XBOOLE_0:def_4; assume n <= m ; ::_thesis: S9 . m in U1 then n < m + 1 by NAT_1:13; then 1 / (m + 1) < 1 / n by A40, XREAL_1:88; then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by A39, PCOMPS_1:1, XXREAL_0:2; then A42: Ball (k9,(1 / (m + 1))) c= U1 by A38, XBOOLE_1:1; h . m = Ball (k9,(1 / (m + 1))) by A30; hence S9 . m in U1 by A42, A41; ::_thesis: verum end; end; rng S9 c= A9 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng S9 or z in A9 ) assume z in rng S9 ; ::_thesis: z in A9 then consider z9 being set such that A43: z9 in dom S9 and A44: z = S9 . z9 by FUNCT_1:def_3; S9 . z9 in (h . z9) /\ A9 by A35, A43; hence z in A9 by A44, XBOOLE_0:def_4; ::_thesis: verum end; hence contradiction by A26, A28, A36; ::_thesis: verum end; consider g being Function such that A45: ( dom g = NAT & ( for k being set st k in NAT holds S1[k,g . k] ) ) from CLASSES1:sch_1(A27); rng g c= bool the carrier of R^1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in bool the carrier of R^1 ) assume z in rng g ; ::_thesis: z in bool the carrier of R^1 then consider k being set such that A46: k in dom g and A47: z = g . k by FUNCT_1:def_3; g . k in the topology of R^1 by A45, A46; hence z in bool the carrier of R^1 by A47; ::_thesis: verum end; then reconsider F = rng g as Subset-Family of R^1 ; F is open proof let O be Subset of R^1; :: according to TOPS_2:def_1 ::_thesis: ( not O in F or O is open ) assume O in F ; ::_thesis: O is open then consider k being set such that A48: k in dom g and A49: O = g . k by FUNCT_1:def_3; g . k in the topology of R^1 by A45, A48; hence O is open by A49, PRE_TOPC:def_2; ::_thesis: verum end; then A50: union F is open by TOPS_2:19; (union F) \ NAT c= REAL \ NAT by TOPMETR:17, XBOOLE_1:33; then ((union F) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9; then reconsider B = ((union F) \ NAT) \/ {REAL} as Subset of REAL? by Def8; reconsider B = B as Subset of REAL? ; A51: B /\ A = {} proof set z = the Element of B /\ A; assume A52: B /\ A <> {} ; ::_thesis: contradiction then A53: the Element of B /\ A in B by XBOOLE_0:def_4; A54: the Element of B /\ A in A by A52, XBOOLE_0:def_4; percases ( the Element of B /\ A in (union F) \ NAT or the Element of B /\ A in {REAL} ) by A53, XBOOLE_0:def_3; suppose the Element of B /\ A in (union F) \ NAT ; ::_thesis: contradiction then the Element of B /\ A in union F by XBOOLE_0:def_5; then consider C being set such that A55: the Element of B /\ A in C and A56: C in F by TARSKI:def_4; consider l being set such that A57: l in dom g and A58: C = g . l by A56, FUNCT_1:def_3; (g . l) /\ A = {} by A45, A57; hence contradiction by A54, A55, A58, XBOOLE_0:def_4; ::_thesis: verum end; suppose the Element of B /\ A in {REAL} ; ::_thesis: contradiction then the Element of B /\ A = REAL by TARSKI:def_1; hence contradiction by A25, A52, XBOOLE_0:def_4; ::_thesis: verum end; end; end; NAT c= union F proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in NAT or k in union F ) assume k in NAT ; ::_thesis: k in union F then ( k in g . k & g . k in rng g ) by A45, FUNCT_1:def_3; hence k in union F by TARSKI:def_4; ::_thesis: verum end; then ( B is open & REAL in B ) by A50, Th28; then A meets B by A1, A25, PRE_TOPC:def_7; hence contradiction by A51, XBOOLE_0:def_7; ::_thesis: verum end; then consider k being Point of R^1 such that A59: k in NAT and A60: ex S9 being sequence of R^1 st ( rng S9 c= A9 & S9 is_convergent_to k ) ; consider S9 being sequence of R^1 such that A61: rng S9 c= A9 and A62: S9 is_convergent_to k by A60; reconsider S = S9 as sequence of REAL? by A61, Th2, XBOOLE_1:1; take S ; ::_thesis: ( rng S c= A & x in Lim S ) thus rng S c= A by A61; ::_thesis: x in Lim S S is_convergent_to x proof let U1 be Subset of REAL?; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 ) assume ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds S . m in U1 then consider O being Subset of R^1 such that A63: ( O is open & NAT c= O ) and A64: U1 = (O \ NAT) \/ {REAL} by A25, Th28; consider n being Element of NAT such that A65: for m being Element of NAT st n <= m holds S9 . m in O by A59, A62, A63, Def3; take n ; ::_thesis: for m being Element of NAT st n <= m holds S . m in U1 thus for m being Element of NAT st n <= m holds S . m in U1 ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in U1 ) assume n <= m ; ::_thesis: S . m in U1 then A66: S9 . m in O by A65; m in NAT ; then m in dom S9 by NORMSP_1:12; then S9 . m in rng S9 by FUNCT_1:def_3; then S9 . m in A9 by A61; then S9 . m in the carrier of REAL? ; then S9 . m in (REAL \ NAT) \/ {REAL} by Def8; then A67: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def_3; S9 . m <> REAL proof A68: S9 . m in REAL by TOPMETR:17; assume S9 . m = REAL ; ::_thesis: contradiction hence contradiction by A68; ::_thesis: verum end; then not S9 . m in NAT by A67, TARSKI:def_1, XBOOLE_0:def_5; then S9 . m in O \ NAT by A66, XBOOLE_0:def_5; hence S . m in U1 by A64, XBOOLE_0:def_3; ::_thesis: verum end; end; hence x in Lim S by Def5; ::_thesis: verum end; end; end; theorem :: FRECHET:34 ex T being non empty TopSpace st ( T is Frechet & not T is first-countable ) by Th32, Th33; begin theorem :: FRECHET:35 for f, g being Function st f tolerates g holds rng (f +* g) = (rng f) \/ (rng g) proof let f, g be Function; ::_thesis: ( f tolerates g implies rng (f +* g) = (rng f) \/ (rng g) ) assume A1: f tolerates g ; ::_thesis: rng (f +* g) = (rng f) \/ (rng g) thus rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; :: according to XBOOLE_0:def_10 ::_thesis: (rng f) \/ (rng g) c= rng (f +* g) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) ) assume A2: x in (rng f) \/ (rng g) ; ::_thesis: x in rng (f +* g) A3: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12; A4: rng g c= rng (f +* g) by FUNCT_4:18; percases ( x in rng g or not x in rng g ) ; suppose x in rng g ; ::_thesis: x in rng (f +* g) hence x in rng (f +* g) by A4; ::_thesis: verum end; supposeA5: not x in rng g ; ::_thesis: x in rng (f +* g) then x in rng f by A2, XBOOLE_0:def_3; then consider a being set such that A6: a in dom f and A7: x = f . a by FUNCT_1:def_3; now__::_thesis:_not_a_in_dom_g assume A8: a in dom g ; ::_thesis: contradiction x = (f +* g) . a by A1, A6, A7, FUNCT_4:15 .= g . a by A8, FUNCT_4:13 ; hence contradiction by A5, A8, FUNCT_1:def_3; ::_thesis: verum end; then a in (dom f) \ (dom g) by A6, XBOOLE_0:def_5; then x in f .: ((dom f) \ (dom g)) by A7, FUNCT_1:def_6; hence x in rng (f +* g) by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem :: FRECHET:36 for r being Real st r > 0 holds ex n being Element of NAT st ( 1 / n < r & n > 0 ) by Lm1;