The abstract of the Mizar article:

The Sequential Closure Operator in Sequential and Frechet Spaces

by

Bartlomiej Skorulski

Received February 13, 1999

MML identifier: FRECHET2

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_1, PRE_TOPC, URYSOHN1, NORMSP_1, FUNCOP_1, FRECHET,
      BOOLE, COMPTS_1, ORDINAL2, SEQM_3, SEQ_1, ARYTM_1, SQUARE_1, CANTOR_1,
      CARD_4, SETFAM_1, ORDINAL1, FINSET_1, SEQ_2, METRIC_1, PCOMPS_1,
      METRIC_6, WAYBEL_7, TARSKI, FUNCT_2, FRECHET2, RLVECT_3, SGRAPH1, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, ORDINAL1,
      ORDINAL2, SETFAM_1, FINSET_1, CARD_4, CQC_SIM1, TOPS_2, RELAT_1, FUNCT_1,
      FUNCT_2, NORMSP_1, COMPTS_1, URYSOHN1, REAL_1, NAT_1, PRE_CIRC, LIMFUNC1,
      CANTOR_1, SEQ_1, SEQM_3, METRIC_1, PCOMPS_1, TBSP_1, STRUCT_0, PRE_TOPC,
      FINSOP_1, METRIC_6, YELLOW_8, FRECHET;
 constructors CARD_4, URYSOHN1, WAYBEL_3, COMPTS_1, TOPS_2, CANTOR_1, SEQ_1,
      NAT_1, FINSOP_1, PRE_CIRC, CQC_SIM1, INT_1, LIMFUNC1, TBSP_1, METRIC_6,
      YELLOW_8, FRECHET;
 clusters XREAL_0, STRUCT_0, PRE_TOPC, NORMSP_1, INT_1, FUNCT_1, METRIC_1,
      PCOMPS_1, GROUP_2, WAYBEL12, FRECHET, RELSET_1, SEQM_3, FUNCT_2,
      MEMBERED, NAT_1, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition
  let T be non empty 1-sorted,f be Function of NAT,NAT, S be sequence of T;
  redefine func S*f -> sequence of T;
end;

theorem :: FRECHET2:1
for T being non empty 1-sorted, S being sequence of T,
NS being increasing Seq_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 Seq_of_Nat;

definition
  let T be non empty 1-sorted, S be sequence of T;
  mode subsequence of S -> sequence of T means
:: FRECHET2:def 1
    ex NS being increasing Seq_of_Nat st it = S * NS;
end;

theorem :: FRECHET2:3
for T being non empty 1-sorted, S being sequence of T holds
  S is subsequence of S;

theorem :: FRECHET2:4
for T being non empty 1-sorted, S being sequence of T,
    S1 being subsequence of S
holds rng S1 c= rng S;

definition
let T be non empty 1-sorted, NS be increasing Seq_of_Nat, S be sequence of T;
redefine func S*NS -> subsequence of S;
end;

theorem :: FRECHET2:5
for T being non empty 1-sorted, S1 being sequence of T,
    S2 being subsequence of S1, S3 being subsequence of S2 holds
      S3 is subsequence of S1;

scheme SubSeqChoice
  {T()->non empty 1-sorted,S()->sequence of T(),P[set]} :
  ex S1 being subsequence of S() st for n being Nat holds P[S1.n]
provided
  for n being Nat ex m being Nat,x being Point of T() st
    n <= m & x = S().m & P[x];

scheme SubSeqChoice1
  {T()->non empty TopStruct,S()->sequence of T(),P[set]} :
  ex S1 being subsequence of S() st
    for n being Nat holds P[S1.n]
provided
 for n being Nat ex m being Nat,x being Point of T() st
    n <= m & x = S().m & P[x];

theorem :: FRECHET2:6
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 Nat st for m being Nat st n <= m holds not S.m in A);

theorem :: FRECHET2:7
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:8
  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_T1;

theorem :: FRECHET2:9
for T being non empty TopSpace st T is_T2 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:10
  for T being non empty TopSpace st T is first-countable holds
  T is_T2 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:11
for T being non empty TopStruct, S being sequence of T st S is not convergent
  holds Lim S = {};

theorem :: FRECHET2:12
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:13
  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:14
for T1,T2 being non empty TopSpace, f being map 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:15
  for T1,T2 being non empty TopSpace, f being map 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 2
  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:16
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:17
for T being non empty TopStruct, A being Subset of T holds
  Cl_Seq(A) c= Cl(A);

theorem :: FRECHET2:18
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:19
for T being non empty TopStruct, S being sequence of T,
S1 being subsequence of S holds
  Lim S c= Lim S1;

theorem :: FRECHET2:20
for T being non empty TopStruct holds
  Cl_Seq({}T) = {};

theorem :: FRECHET2:21
for T being non empty TopStruct, A being Subset of T holds
  A c= Cl_Seq(A);

theorem :: FRECHET2:22
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:23
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:24
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:25
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:26
  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 that
 ex x being Point of T st Lim S = {x};
func lim S -> Point of T means
:: FRECHET2:def 3
  S is_convergent_to it;
end;

theorem :: FRECHET2:27
for T being non empty TopSpace st T is_T2
for S being sequence of T st S is convergent holds
  ex x being Point of T st Lim S = {x};

theorem :: FRECHET2:28
for T being non empty TopSpace st T is_T2
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:29
  for M being MetrStruct,S being sequence of M holds
  S is sequence of TopSpaceMetr(M);

theorem :: FRECHET2:30
  for M being non empty MetrStruct,S being sequence of TopSpaceMetr(M) holds
  S is sequence of M;

theorem :: FRECHET2:31
for M being non empty MetrSpace,S being sequence of M, x being Point of M,
  S' being sequence of TopSpaceMetr(M), x' being Point of TopSpaceMetr(M)
    st S = S' & x = x' holds
  S is_convergent_in_metrspace_to x iff S' is_convergent_to x';

theorem :: FRECHET2:32
  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:33
  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 4
  for O being Subset of T, n being Nat st O is open & x in O
    ex m being Nat st n <= m & S.m in O;
end;

theorem :: FRECHET2:34
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:35
  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:36
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:37
for T being non empty TopStruct, S being sequence of T, x,y being Point of T
  st for n being Nat holds S.n = y & S is_convergent_to x holds
    x in Cl({y});

theorem :: FRECHET2:38
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:39
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 PermSeq
  {T()->non empty 1-sorted,S()->sequence of T(),p()->Permutation of NAT,
   P[set]} :
  ex n being Nat st for m being Nat st n<=m holds P[(S()*p()).m]
provided
  ex n being Nat st for m being Nat, x being Point of T()
    st n<=m & x=S().m holds P[x];

scheme PermSeq2
  {T()->non empty TopStruct,S()->sequence of T(),p()->Permutation of NAT,
   P[set]} :
  ex n being Nat st for m being Nat st n<=m holds P[(S()*p()).m]
provided
  ex n being Nat st for m being Nat, x being Point of T()
    st n<=m & x=S().m holds P[x];

theorem :: FRECHET2:40
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:41
for n0 being Nat ex NS being increasing Seq_of_Nat st
  for n being Nat holds NS.n=n+n0;

theorem :: FRECHET2:42
for T being non empty 1-sorted, S being sequence of T, n0 being Nat
ex S1 being subsequence of S st
  for n being Nat holds S1.n=S.(n+n0);

theorem :: FRECHET2:43
for T being non empty TopStruct, S being sequence of T, x being Point of T,
    S1 being subsequence of S st
      x is_a_cluster_point_of S &
      ex n0 being Nat st for n being Nat holds S1.n=S.(n+n0)
holds x is_a_cluster_point_of S1;

theorem :: FRECHET2:44
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:45
  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:46
  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 Nat st m >= n holds S.m c= S.n;

theorem :: FRECHET2:47
  for T being non empty TopSpace holds
  T is_T1 iff for p being Point of T holds Cl({p}) = {p};

theorem :: FRECHET2:48
  for T being non empty TopSpace holds
  T is_T2 implies T is_T1;

theorem :: FRECHET2:49
  for T being non empty TopSpace st not T is_T1 holds
  ex x1,x2 being Point of T, S being sequence of T st
     S = (NAT --> x1) & x1 <> x2 & S is_convergent_to x2;

theorem :: FRECHET2:50
  for f being Function st dom f is infinite & f is one-to-one holds
  rng f is infinite;

theorem :: FRECHET2:51
  for X being non empty finite Subset of NAT, x being Nat holds
  x in X implies x <= max X;