:: First-countable, Sequential, and { F } rechet Spaces :: by Bart{\l}omiej Skorulski :: :: Received May 13, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XXREAL_0, CARD_1, SUBSET_1, ARYTM_3, XBOOLE_0, STRUCT_0, NAT_1, RELAT_1, TARSKI, PRE_TOPC, RLVECT_3, RCOMP_1, SETFAM_1, FUNCT_1, ZFMISC_1, METRIC_1, XXREAL_1, ARYTM_1, COMPLEX1, TOPMETR, PCOMPS_1, ORDINAL1, CARD_3, FUNCT_4, FUNCOP_1, SEQ_2, PARTFUN1, FRECHET, YELLOW_8; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, CARD_3, FUNCT_4, RCOMP_1, PRE_TOPC, TOPS_2, METRIC_1, PCOMPS_1, TOPMETR, YELLOW_8, XXREAL_0; constructors FUNCT_4, REAL_1, NAT_1, MEMBERED, COMPLEX1, RCOMP_1, PCOMPS_1, FUNCOP_1, CARD_3, TOPS_2, TOPMETR, YELLOW_8, BINOP_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, TOPMETR, RELSET_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: :: Preliminaries :: theorem :: FRECHET:1 for T being non empty 1-sorted,S being sequence of T holds rng S is Subset of T; theorem :: FRECHET:2 for T1 being non empty 1-sorted, T2 being 1-sorted, S being sequence of T1 st rng S c= the carrier of T2 holds S is sequence of T2; theorem :: FRECHET:3 for T being non empty TopSpace, x being Point of T, B being Basis of x holds B <> {}; registration let T be non empty TopSpace; let x be Point of T; cluster -> non empty for Basis of x; end; theorem :: FRECHET:4 for T being TopSpace, A,B being Subset of T st A is open & B is closed holds A \ B is open; theorem :: 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; theorem :: FRECHET:6 for T being TopSpace, S being non empty TopStruct, 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; theorem :: FRECHET:7 for x being Point of RealSpace, r being Real holds Ball(x,r) = ].x-r, x+r.[; theorem :: FRECHET:8 for A being Subset of R^1 holds A is open iff for x being Real st x in A ex r being Real st r >0 & ].x-r, x+r.[ c= A; theorem :: 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; theorem :: FRECHET:10 for B being Subset of R^1 holds B = NAT implies B is closed; definition let M be non empty MetrStruct, x be Point of TopSpaceMetr(M); func Balls(x) -> Subset-Family of TopSpaceMetr(M) means :: FRECHET:def 1 ex y being Point of M st y = x & it = { Ball(y,1/n) where n is Nat: n <> 0 }; end; registration let M be non empty MetrSpace, x be Point of TopSpaceMetr(M); cluster Balls(x) -> open x -quasi_basis; end; registration let M be non empty MetrSpace, x be Point of TopSpaceMetr(M); cluster Balls(x) -> countable; end; theorem :: FRECHET:11 for M being non empty MetrSpace, x being Point of TopSpaceMetr(M), x9 being Point of M st x = x9 ex f being sequence of Balls(x) st for n being Element of NAT holds f.n = Ball(x9,1/(n+1)); theorem :: FRECHET:12 for f,g being Function holds rng(f+*g)=f.:(dom f\dom g) \/ rng g; theorem :: FRECHET:13 for A,B being set holds B c= A implies (id A).:(B) = B; theorem :: FRECHET:14 for A,B,x being set holds dom((id A)+*(B --> x)) = A \/ B; theorem :: FRECHET:15 for A,B,x being set st B <> {} holds rng((id A)+*(B --> x)) = (A \ B) \/ {x}; theorem :: FRECHET:16 for A,B,C,x being set holds C c= A implies ((id A)+*(B --> x))"( C \ {x}) = C \ B \ {x}; theorem :: FRECHET:17 for A,B,x being set holds not x in A implies ((id A)+*(B --> x)) "({x}) = B; theorem :: FRECHET:18 for A,B,C,x being set holds C c= A & not x in A implies ((id A) +*(B --> x))"(C \/ {x}) = C \/ B; theorem :: FRECHET:19 for A,B,C,x being set holds C c= A & not x in A implies ((id A) +*(B --> x))"(C \ {x}) = C \ B; begin :: :: Convergent Sequences in Topological Spaces, :: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES :: definition let T be non empty TopStruct; attr T is first-countable means :: FRECHET:def 2 for x be Point of T ex B be Basis of x st B is countable; end; theorem :: FRECHET:20 for M being non empty MetrSpace holds TopSpaceMetr(M) is first-countable; theorem :: FRECHET:21 R^1 is first-countable; registration cluster R^1 -> first-countable; end; definition let T be TopStruct, S be sequence of T, x be Point of T; pred S is_convergent_to x means :: FRECHET:def 3 for U1 being Subset of T st U1 is open & x in U1 ex n being Nat st for m being Nat st n <= m holds S.m in U1; end; theorem :: FRECHET:22 for T being non empty TopStruct, x being Point of T, S being sequence of T holds S = (NAT --> x) implies S is_convergent_to x; definition let T be TopStruct, S be sequence of T; attr S is convergent means :: FRECHET:def 4 ex x being Point of T st S is_convergent_to x; end; definition let T be non empty TopStruct, S be sequence of T; func Lim S -> Subset of T means :: FRECHET:def 5 for x being Point of T holds x in it iff S is_convergent_to x; end; definition let T be non empty TopStruct; attr T is Frechet means :: FRECHET:def 6 for A being Subset of T,x being Point of T st x in Cl(A) ex S being sequence of T st rng S c= A & x in Lim S; end; definition let T be non empty TopStruct; attr T 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; theorem :: FRECHET:23 for T being non empty TopSpace holds T is first-countable implies T is Frechet; registration cluster first-countable -> Frechet for non empty TopSpace; end; theorem :: FRECHET:24 for T being non empty TopSpace,A being Subset of T holds A is closed implies for S being sequence of T st rng S c= A holds Lim S c= A; theorem :: FRECHET:25 for T being non empty TopSpace holds (for A being Subset of T holds (for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A) implies A is closed) implies T is sequential; theorem :: FRECHET:26 for T being non empty TopSpace holds T is Frechet implies T is sequential; registration cluster Frechet -> sequential for non empty TopSpace; end; begin :: :: Not (for T holds T is Frechet implies T is first-countable) :: definition func REAL? -> strict non empty TopSpace means :: 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; end; theorem :: FRECHET:27 REAL is Point of REAL?; theorem :: 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}; theorem :: 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 = {}; theorem :: FRECHET:30 for A being Subset of R^1,B being Subset of REAL? st A = B holds NAT /\ A = {} & A is open iff not REAL in B & B is open; theorem :: FRECHET:31 for A being Subset of REAL? st A = {REAL} holds A is closed; theorem :: FRECHET:32 REAL? is not first-countable; theorem :: FRECHET:33 REAL? is Frechet; theorem :: FRECHET:34 not (for T being non empty TopSpace holds T is Frechet implies T is first-countable); 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); theorem :: FRECHET:36 for r being Real st r>0 ex n being Nat st 1/n < r & n>0;