:: First-countable, Sequential, and { F } rechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received May 13, 1998
:: Copyright (c) 1998-2016 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;