:: The Sequential Closure Operator In Sequential and Frechet Spaces
::  by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999-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 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;