:: The Sequential Closure Operator In Sequential and Frechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999-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 XBOOLE_0, PRE_TOPC, RCOMP_1, TARSKI, NAT_1, NUMBERS, FUNCOP_1,
FRECHET, SUBSET_1, CARD_1, STRUCT_0, ORDINAL2, RELAT_1, SEQ_1, VALUED_0,
XXREAL_0, FUNCT_1, RLVECT_3, CARD_3, SETFAM_1, ORDINAL1, ZFMISC_1,
FINSET_1, ARYTM_3, SEQ_2, METRIC_1, PCOMPS_1, METRIC_6, XREAL_0, REAL_1,
WAYBEL_7, ARYTM_1, FUNCT_2, FRECHET2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, SETFAM_1, FINSET_1, CARD_3, TOPS_2, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, SEQ_1, FUNCT_2, NAT_1, XXREAL_2, VALUED_0, METRIC_1,
PCOMPS_1, TBSP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, FUNCOP_1, METRIC_6,
YELLOW_8, FRECHET, SEQ_4;
constructors SETFAM_1, REALSET1, CARD_3, TOPS_2, TBSP_1, METRIC_6, YELLOW_8,
FRECHET, SEQ_4, RELSET_1, FUNCOP_1, NUMBERS;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, FRECHET, VALUED_0, CARD_1,
XXREAL_2, ORDINAL1, FINSET_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
theorem :: FRECHET2:1
for T being non empty 1-sorted, S being sequence of T, NS being
increasing sequence of NAT holds S*NS is sequence of T;
theorem :: FRECHET2:2
for RS being Real_Sequence st RS=id NAT holds RS is increasing
sequence of NAT;
theorem :: FRECHET2:3
for T being non empty 1-sorted, S being sequence of T, A being
Subset of T holds (for S1 being subsequence of S holds not rng S1 c= A) implies
ex n being Element of NAT st for m being Element of NAT st n <= m holds not S.m
in A;
theorem :: FRECHET2:4
for T being non empty 1-sorted,S being sequence of T, A,B being
Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st rng S1 c=
A or rng S1 c= B;
theorem :: FRECHET2:5
for T being non empty TopSpace holds (for S being sequence of T holds
for x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2))
implies T is T_1;
theorem :: FRECHET2:6
for T being non empty TopSpace st T is T_2 holds for S being
sequence of T, x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies
x1=x2);
theorem :: FRECHET2:7
for T being non empty TopSpace st T is first-countable holds T is T_2
iff for S being sequence of T holds for x1,x2 being Point of T holds (x1 in Lim
S & x2 in Lim S implies x1=x2);
theorem :: FRECHET2:8
for T being non empty TopStruct, S being sequence of T st S is
not convergent holds Lim S = {};
theorem :: FRECHET2:9
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 :: FRECHET2:10
for T being non empty TopStruct,S being sequence of T, x being Point
of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2
being subsequence of S1 holds not S2 is_convergent_to x;
begin ::The Continuous Maps
theorem :: FRECHET2:11
for T1,T2 being non empty TopSpace, f being Function of T1,T2
holds f is continuous implies for S1 being sequence of T1, S2 being sequence of
T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2;
theorem :: FRECHET2:12
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st T1 is
sequential holds f is continuous iff for S1 being sequence of T1, S2 being
sequence of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2;
begin ::The Sequential Closure Operator
definition
let T be non empty TopStruct, A be Subset of T;
func Cl_Seq A -> Subset of T means
:: FRECHET2:def 1
for x being Point of T holds x in
it iff ex S being sequence of T st rng S c= A & x in Lim S;
end;
theorem :: FRECHET2:13
for T being non empty TopStruct, A being Subset of T, S being
sequence of T, x being Point of T st rng S c= A & x in Lim S holds x in Cl(A)
;
theorem :: FRECHET2:14
for T being non empty TopStruct, A being Subset of T holds Cl_Seq(A) c= Cl(A)
;
theorem :: FRECHET2:15
for T being non empty TopStruct, S being sequence of T, S1 being
subsequence of S, x being Point of T holds S is_convergent_to x implies S1
is_convergent_to x;
theorem :: FRECHET2:16
for T being non empty TopStruct, S being sequence of T, S1 being
subsequence of S holds Lim S c= Lim S1;
theorem :: FRECHET2:17
for T being non empty TopStruct holds Cl_Seq({}T) = {};
theorem :: FRECHET2:18
for T being non empty TopStruct, A being Subset of T holds A c= Cl_Seq(A);
theorem :: FRECHET2:19
for T being non empty TopStruct, A,B being Subset of T holds
Cl_Seq(A) \/ Cl_Seq(B) = Cl_Seq(A \/ B);
theorem :: FRECHET2:20
for T being non empty TopStruct holds T is Frechet iff for A
being Subset of T holds Cl(A)=Cl_Seq(A);
theorem :: FRECHET2:21
for T being non empty TopSpace st T is Frechet holds for A,B
being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B) =
Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A);
theorem :: FRECHET2:22
for T being non empty TopSpace st T is sequential holds (for A
being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)) implies T is Frechet;
theorem :: FRECHET2:23
for T being non empty TopSpace st T is sequential holds T is Frechet
iff for A,B being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(
A \/ B) = Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A);
begin ::The Limit
definition
let T be non empty TopSpace, S be sequence of T;
assume
ex x being Point of T st Lim S = {x};
func lim S -> Point of T means
:: FRECHET2:def 2
S is_convergent_to it;
end;
theorem :: FRECHET2:24
for T being non empty TopSpace st T is T_2 for S being sequence
of T st S is convergent holds ex x being Point of T st Lim S = {x};
theorem :: FRECHET2:25
for T being non empty TopSpace st T is T_2 for S being sequence
of T,x being Point of T holds S is_convergent_to x iff S is convergent & x =
lim S;
theorem :: FRECHET2:26
for M being MetrStruct,S being sequence of M holds S is sequence of
TopSpaceMetr(M);
theorem :: FRECHET2:27
for M being non empty MetrStruct,S being sequence of TopSpaceMetr(M)
holds S is sequence of M;
theorem :: FRECHET2:28
for M being non empty MetrSpace,S being sequence of M, x being
Point of M, S9 being sequence of TopSpaceMetr(M), x9 being Point of
TopSpaceMetr(M) st S = S9 & x = x9 holds S is_convergent_in_metrspace_to x iff
S9 is_convergent_to x9;
theorem :: FRECHET2:29
for M being non empty MetrSpace,Sm being sequence of M, St being
sequence of TopSpaceMetr(M) st Sm=St holds Sm is convergent iff St is
convergent;
theorem :: FRECHET2:30
for M being non empty MetrSpace,Sm being sequence of M, St being
sequence of TopSpaceMetr(M) st Sm=St & Sm is convergent holds lim Sm = lim St
;
begin ::The Cluster Points
definition
let T be TopStruct, S be sequence of T, x be Point of T;
pred x is_a_cluster_point_of S means
:: FRECHET2:def 3
for O being Subset of T, n being Nat st O is open & x in O
ex m being Element of NAT st n <= m & S.m
in O;
end;
theorem :: FRECHET2:31
for T being non empty TopStruct, S being sequence of T, x being
Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x
is_a_cluster_point_of S;
theorem :: FRECHET2:32
for T being non empty TopStruct, S being sequence of T, x being Point
of T st S is_convergent_to x holds x is_a_cluster_point_of S;
theorem :: FRECHET2:33
for T being non empty TopStruct, S being sequence of T, x being
Point of T, Y being Subset of T st Y = {y where y is Point of T : x in Cl({y})
} & rng S c= Y holds S is_convergent_to x;
theorem :: FRECHET2:34
for T being non empty TopStruct, S being sequence of T, x,y
being Point of T st for n being Element of NAT holds S.n = y & S
is_convergent_to x holds x in Cl({y});
theorem :: FRECHET2:35
for T being non empty TopStruct, x being Point of T, Y being
Subset of T, S being sequence of T st Y = { y where y is Point of T : x in Cl({
y}) } & rng S misses Y & S is_convergent_to x ex S1 being subsequence of S st
S1 is one-to-one;
theorem :: FRECHET2:36
for T being non empty TopStruct, S1,S2 being sequence of T st
rng S2 c= rng S1 & S2 is one-to-one ex P being Permutation of NAT st S2*P is
subsequence of S1;
scheme :: FRECHET2:sch 1
PermSeq {T()->non empty 1-sorted,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
holds P[(S()*p()).m]
provided
ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x];
scheme :: FRECHET2:sch 2
PermSeq2 {T()->non empty TopStruct,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
holds P[(S()*p()).m]
provided
ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x];
theorem :: FRECHET2:37
for T being non empty TopStruct, S being sequence of T, P being
Permutation of NAT, x being Point of T st S is_convergent_to x holds S*P
is_convergent_to x;
theorem :: FRECHET2:38
for n0 being Element of NAT ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS.n=n+n0;
theorem :: FRECHET2:39
for T being non empty TopStruct, S being sequence of T, x being
Point of T, n0 being Nat st x is_a_cluster_point_of S holds x
is_a_cluster_point_of S^\n0;
theorem :: FRECHET2:40
for T being non empty TopStruct, S being sequence of T, x being
Point of T st x is_a_cluster_point_of S holds x in Cl(rng S);
theorem :: FRECHET2:41
for T being non empty TopStruct st T is Frechet for S being sequence
of T, x being Point of T st x is_a_cluster_point_of S holds ex S1 being
subsequence of S st S1 is_convergent_to x;
begin :: Auxiliary theorems
theorem :: FRECHET2:42
for T being non empty TopSpace st T is first-countable holds for x
being Point of T holds ex B being Basis of x st ex S being Function st dom S =
NAT & rng S = B & for n,m being Element of NAT st m >= n holds S.m c= S.n;
theorem :: FRECHET2:43
for T being non empty TopSpace st for p being Point of T holds Cl({p})
= {p} holds T is T_1;
theorem :: FRECHET2:44
for T being non empty TopSpace holds T is T_2 implies T is T_1;
theorem :: FRECHET2:45
for T being non empty TopSpace st not T is T_1 holds ex x1,x2 being
Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S
is_convergent_to x2;