:: First-countable, Sequential, and { F } rechet Spaces :: by Bart{\l}omiej Skorulski :: :: Received May 13, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin Lm1: for r being Real st r > 0 holds ex n being Element of NAT st ( 1 / n < r & n > 0 ) proofend; :: :: Preliminaries :: 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 proofend; theorem Th3: :: FRECHET:3 for T being non empty TopSpace for x being Point of T for B being Basis of x holds B <> {} proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th7: :: FRECHET:7 for x being Point of RealSpace for r being Real holds Ball (x,r) = ].(x - r),(x + r).[ proofend; 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 ) ) proofend; 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 proofend; theorem Th10: :: FRECHET:10 for B being Subset of R^1 st B = NAT holds B is closed proofend; 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 } ) proofend; 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 ) proofend; end; registration let M be non empty MetrSpace; let x be Point of (TopSpaceMetr M); cluster Balls x -> countable ; coherence Balls x is countable proofend; 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))) proofend; theorem Th12: :: FRECHET:12 for f, g being Function holds rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) proofend; theorem Th13: :: FRECHET:13 for A, B being set st B c= A holds (id A) .: B = B proofend; theorem Th14: :: FRECHET:14 for A, B, x being set holds dom ((id A) +* (B --> x)) = A \/ B proofend; theorem Th15: :: FRECHET:15 for A, B, x being set st B <> {} holds rng ((id A) +* (B --> x)) = (A \ B) \/ {x} proofend; 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} proofend; theorem Th17: :: FRECHET:17 for A, B, x being set st not x in A holds ((id A) +* (B --> x)) " {x} = B proofend; 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 proofend; 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 proofend; begin :: :: Convergent Sequences in Topological Spaces, :: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES :: 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th26: :: FRECHET:26 for T being non empty TopSpace st T is Frechet holds T is sequential proofend; 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 :: :: Not (for T holds T is Frechet implies T is first-countable) :: 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 ) ) ) ) proofend; 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 proofend; 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? proofend; theorem Th27: :: FRECHET:27 REAL is Point of REAL? proofend; 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} ) ) proofend; 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 = {} ) ) proofend; 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 ) ) proofend; theorem Th31: :: FRECHET:31 for A being Subset of REAL? st A = {REAL} holds A is closed proofend; theorem Th32: :: FRECHET:32 not REAL? is first-countable proofend; theorem Th33: :: FRECHET:33 REAL? is Frechet proofend; theorem :: FRECHET:34 ex T being non empty TopSpace st ( T is Frechet & not T is first-countable ) by Th32, Th33; begin :: :: Auxiliary theorems :: ::Moved from CIRCCMB2:5, AK, 20.02.2006 theorem :: FRECHET:35 for f, g being Function st f tolerates g holds rng (f +* g) = (rng f) \/ (rng g) proofend; 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;