Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

The abstract of the Mizar article:

On the Kuratowski Limit Operators

by
Adam Grabowski

Received August 12, 2003

MML identifier: KURATO_2
[ Mizar article, MML identifier index ]


environ

 vocabulary KURATO_2, WELLFND1, FRECHET2, REARRAN1, YELLOW_6, BOOLE, EUCLID,
      PRE_TOPC, COMPTS_1, SETFAM_1, METRIC_1, SUBSET_1, PCOMPS_1, RELAT_1,
      ORDINAL2, LATTICES, SEQ_2, PROB_1, SEQ_1, FUNCT_1, SEQM_3, FRECHET,
      ARYTM_3, CONNSP_2, ARYTM, TOPS_1, ARYTM_1, NEWTON, NORMSP_1, COMPLEX1,
      INT_1, FINSEQ_1, TOPREAL1, TOPREAL2, JORDAN9, JORDAN2C, SQUARE_1,
      GOBOARD9, ZF_REFLE, FUNCOP_1, MCART_1, WAYBEL_7;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1,
      XREAL_0, REAL_1, NAT_1, SETFAM_1, MCART_1, STRUCT_0, PRE_TOPC, TOPS_1,
      COMPTS_1, RELAT_1, FUNCT_1, INT_1, FINSEQ_1, SEQ_1, TBSP_1, PARTFUN1,
      FUNCT_2, METRIC_1, PCOMPS_1, EUCLID, NORMSP_1, BORSUK_1, PROB_1,
      PSCOMP_1, LIMFUNC1, CONNSP_2, TOPREAL1, TOPREAL2, JORDAN2C, SEQM_3,
      GOBOARD9, FRECHET, FRECHET2, TOPRNS_1, JORDAN9, FUNCT_6, YELLOW_6;
 constructors REAL_1, JORDAN2C, GROUP_1, TOPREAL2, CONNSP_1, PSCOMP_1, TOPS_1,
      WEIERSTR, PROB_1, TOPRNS_1, FRECHET, NAT_1, JORDAN9, TBSP_1, CQC_SIM1,
      LIMFUNC1, GOBOARD9, YELLOW_6, FUNCT_6, FRECHET2;
 clusters XREAL_0, RELSET_1, NAT_1, INT_1, JORDAN1B, SUBSET_1, STRUCT_0,
      TOPS_1, BORSUK_1, EUCLID, FINSET_1, METRIC_1, TOPREAL6, GOBRD14,
      HAUSDORF, SEQ_1, SEQM_3, MEMBERED, FUNCT_2, PARTFUN1, ORDINAL2;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;


begin :: Preliminaries

theorem :: KURATO_2:1
  for X, x being set,
      A being Subset of X st not x in A & x in X holds x in A`;

theorem :: KURATO_2:2
  for F being Function,
      i being set st i in dom F holds meet F c= F.i;

theorem :: KURATO_2:3
  for T being non empty 1-sorted,
      S1, S2 being SetSequence of the carrier of T holds
    S1 = S2 iff for n being Nat holds S1.n = S2.n;

theorem :: KURATO_2:4
  for A, B, C, D being set st A meets B & C meets D holds
    [: A, C :] meets [: B, D :];

definition let X be 1-sorted;
  cluster -> non empty SetSequence of the carrier of X;
end;

definition let T be non empty 1-sorted;
  cluster non-empty SetSequence of the carrier of T;
end;

definition let T be non empty 1-sorted;
  mode SetSequence of T is SetSequence of the carrier of T;
  canceled;
end;

scheme LambdaSSeq { X() -> non empty 1-sorted,
                    F(set) -> Subset of X() } :
  ex f being SetSequence of X() st
    for n being Nat holds f.n = F(n);

scheme ExTopStrSeq { R() -> non empty TopSpace,
                     F(set) -> Subset of R() } :
   ex S be SetSequence of the carrier of R() st
     for n be Nat holds S.n = F(n);

theorem :: KURATO_2:5
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X holds
    rng F is Subset-Family of X;

definition let X be non empty 1-sorted,
               F be SetSequence of the carrier of X;
  redefine func Union F -> Subset of X;
  redefine func meet F -> Subset of X;
end;

begin :: Lower and Upper Limit of Sequences of Subsets

definition let X be non empty set;
           let S be Function of NAT, X;
           let k be Nat;
  func S ^\ k -> Function of NAT, X means
:: KURATO_2:def 2
  for n being Nat holds it.n = S.(n + k);
end;

definition let X be non empty 1-sorted,
               F be SetSequence of the carrier of X;
  func lim_inf F -> Subset of X means
:: KURATO_2:def 3
    ex f being SetSequence of X st it = Union f &
      for n being Nat holds f.n = meet (F ^\ n);
  func lim_sup F -> Subset of X means
:: KURATO_2:def 4
    ex f being SetSequence of X st it = meet f &
      for n being Nat holds f.n = Union (F ^\ n);
end;

theorem :: KURATO_2:6
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X,
      x being set holds
   x in meet F iff for z being Nat holds x in F.z;

theorem :: KURATO_2:7
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X,
      x being set holds
   x in lim_inf F iff ex n being Nat st for k being Nat holds x in F.(n+k);

theorem :: KURATO_2:8
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X,
      x being set holds
   x in lim_sup F iff for n being Nat ex k being Nat st x in F.(n+k);

theorem :: KURATO_2:9
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X holds
   lim_inf F c= lim_sup F;

theorem :: KURATO_2:10
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X holds
   meet F c= lim_inf F;

theorem :: KURATO_2:11
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X holds
   lim_sup F c= Union F;

theorem :: KURATO_2:12
  for X being non empty 1-sorted,
      F being SetSequence of the carrier of X holds
    lim_inf F = (lim_sup Complement F)`;

theorem :: KURATO_2:13
  for X being non empty 1-sorted,
      A, B, C being SetSequence of the carrier of X st
   (for n being Nat holds C.n = A.n /\ B.n) holds
     lim_inf C = lim_inf A /\ lim_inf B;

theorem :: KURATO_2:14
  for X being non empty 1-sorted,
      A, B, C being SetSequence of the carrier of X st
   (for n being Nat holds C.n = A.n \/ B.n) holds
     lim_sup C = lim_sup A \/ lim_sup B;

theorem :: KURATO_2:15
  for X being non empty 1-sorted,
      A, B, C being SetSequence of the carrier of X st
   (for n being Nat holds C.n = A.n \/ B.n) holds
     lim_inf A \/ lim_inf B c= lim_inf C;

theorem :: KURATO_2:16
  for X being non empty 1-sorted,
      A, B, C being SetSequence of the carrier of X st
   (for n being Nat holds C.n = A.n /\ B.n) holds
     lim_sup C c= lim_sup A /\ lim_sup B;

theorem :: KURATO_2:17
  for X being non empty 1-sorted,
      A being SetSequence of the carrier of X,
      B being Subset of X st
   (for n being Nat holds A.n = B) holds
     lim_sup A = B;

theorem :: KURATO_2:18
  for X being non empty 1-sorted,
      A being SetSequence of the carrier of X,
      B being Subset of X st
   (for n being Nat holds A.n = B) holds
     lim_inf A = B;

theorem :: KURATO_2:19
  for X being non empty 1-sorted,
      A, B being SetSequence of the carrier of X,
      C being Subset of X st
   (for n being Nat holds B.n = C \+\ A.n) holds
     C \+\ lim_inf A c= lim_sup B;

theorem :: KURATO_2:20
  for X being non empty 1-sorted,
      A, B being SetSequence of the carrier of X,
      C being Subset of X st
   (for n being Nat holds B.n = C \+\ A.n) holds
     C \+\ lim_sup A c= lim_sup B;

begin :: Ascending and Descending Families of Subsets

definition let T be non empty 1-sorted,
               S be SetSequence of T;
  attr S is descending means
:: KURATO_2:def 5
    for i being Nat holds S.(i+1) c= S.i;
  attr S is ascending means
:: KURATO_2:def 6
    for i being Nat holds S.i c= S.(i+1);
end;

theorem :: KURATO_2:21
  for f being Function st (for i being Nat holds f.(i+1) c= f.i)
    for i, j being Nat st
      i <= j holds f.j c= f.i;

theorem :: KURATO_2:22
  for T being non empty 1-sorted,
      C being SetSequence of T st
      C is descending holds
    for i, m being Nat st i >= m holds
      C.i c= C.m;

theorem :: KURATO_2:23
  for T being non empty 1-sorted,
      C being SetSequence of T st
      C is ascending holds
    for i, m being Nat st i >= m holds
      C.m c= C.i;

theorem :: KURATO_2:24
  for T being non empty 1-sorted,
      F being SetSequence of T,
      x being set st
    F is descending &
    ex k being Nat st for n being Nat st n > k holds x in F.n holds
      x in meet F;

theorem :: KURATO_2:25
  for T being non empty 1-sorted,
      F being SetSequence of T st
    F is descending holds
      lim_inf F = meet F;

theorem :: KURATO_2:26
  for T being non empty 1-sorted,
      F being SetSequence of T st
    F is ascending holds
      lim_sup F = Union F;

begin :: Constant and Convergent Sequences

definition let T be non empty 1-sorted,
               S be SetSequence of T;
  attr S is convergent means
:: KURATO_2:def 7
  lim_sup S = lim_inf S;
end;

theorem :: KURATO_2:27
  for T being non empty 1-sorted,
      S being SetSequence of T st S is constant holds
    the_value_of S is Subset of T;

definition let T be non empty 1-sorted,
               S be SetSequence of T;
  redefine attr S is constant means
:: KURATO_2:def 8
  ex A being Subset of T st for n being Nat holds S.n = A;
end;

definition let T be non empty 1-sorted;
  cluster constant -> convergent ascending descending SetSequence of T;
end;

definition let T be non empty 1-sorted;
  cluster constant non empty SetSequence of T;
end;

definition let T be non empty 1-sorted,
               S be convergent SetSequence of T;
  func Lim_K S -> Subset of T means
:: KURATO_2:def 9
  it = lim_sup S & it = lim_inf S;
end;

theorem :: KURATO_2:28
  for X being non empty 1-sorted,
      F being convergent SetSequence of X,
      x being set holds
   x in Lim_K F iff ex n being Nat st for k being Nat holds x in F.(n+k);

begin :: Topological Lemmas

 reserve n for Nat;

definition let f be FinSequence of the carrier of TOP-REAL 2;
  cluster L~f -> closed;
end;

theorem :: KURATO_2:29
  for r being real number,
      M being non empty Reflexive MetrStruct,
      x being Element of M st 0 < r holds
   x in Ball (x,r);

theorem :: KURATO_2:30
  for x being Point of Euclid n,
      r being real number holds
   Ball (x, r) is open Subset of TOP-REAL n;

theorem :: KURATO_2:31
  for p, q being Point of TOP-REAL n,
      p', q' being Point of Euclid n st
   p = p' & q = q' holds
     dist (p', q') = |. p - q .|;

theorem :: KURATO_2:32
  for p being Point of Euclid n,
      x, p' being Point of TOP-REAL n,
      r being real number st
    p = p' & x in Ball (p, r) holds
      |. x - p' .| < r;

theorem :: KURATO_2:33
  for p being Point of Euclid n,
      x, p' being Point of TOP-REAL n,
      r being real number st
    p = p' & |. x - p' .| < r holds
      x in Ball (p, r);

theorem :: KURATO_2:34
  for n being Nat,
      r being Point of TOP-REAL n,
      X being Subset of TOP-REAL n st r in Cl X holds
   ex seq being Real_Sequence of n st
      rng seq c= X & seq is convergent & lim seq = r;

definition let M be non empty MetrSpace;
  cluster TopSpaceMetr M -> first-countable;
end;

definition let n be Nat;
  cluster TOP-REAL n -> first-countable;
end;

theorem :: KURATO_2:35
  for p being Point of Euclid n,
      q being Point of TOP-REAL n,
      r being real number st
    p = q & r > 0 holds
  Ball (p, r) is a_neighborhood of q;

theorem :: KURATO_2:36
  for A being Subset of TOP-REAL n,
      p being Point of TOP-REAL n,
      p' being Point of Euclid n st p = p' holds
  p in Cl A iff
    for r being real number st r > 0 holds Ball (p', r) meets A;

theorem :: KURATO_2:37
  for x, y being Point of TOP-REAL n,
      x' being Point of Euclid n st x' = x & x <> y
    ex r being Real st not y in Ball (x', r);

theorem :: KURATO_2:38
  for S being Subset of TOP-REAL n holds
    S is non Bounded iff
    for r being Real st r > 0 holds
     ex x, y being Point of Euclid n st
        x in S & y in S & dist (x, y) > r;

theorem :: KURATO_2:39
  for a, b being real number,
      x, y being Point of Euclid n st
    Ball (x, a) meets Ball (y, b) holds
  dist (x, y) < a + b;

theorem :: KURATO_2:40
  for a, b, c being real number,
      x, y, z being Point of Euclid n st
    Ball (x, a) meets Ball (z, c) & Ball (z, c) meets Ball (y, b) holds
  dist (x, y) < a + b + 2*c;

theorem :: KURATO_2:41
  for X, Y being non empty TopSpace,
      x being Point of X,
      y being Point of Y,
      V being Subset of [: X, Y :] holds
    V is a_neighborhood of [: {x}, {y} :] iff
      V is a_neighborhood of [ x, y ];

scheme TSubsetEx { S() -> non empty TopStruct, P[set] } :
  ex X being Subset of S() st
   for x being Point of S() holds x in X iff P[x];

scheme TSubsetUniq { S() -> TopStruct, P[set] } :
  for A1, A2 being Subset of S() st
  (for x being Point of S() holds x in A1 iff P[x]) &
  (for x being Point of S() holds x in A2 iff P[x]) holds
    A1 = A2;

definition let T be non empty TopStruct;
           let S be SetSequence of the carrier of T;
           let i be Nat;
 redefine func S.i -> Subset of T;
end;

theorem :: KURATO_2:42
  for T be non empty 1-sorted,
      S being SetSequence of the carrier of T,
      R being Seq_of_Nat holds
    S * R is SetSequence of T;

theorem :: KURATO_2:43
  id NAT is increasing Seq_of_Nat;

definition
  cluster id NAT -> real-yielding;
end;

begin :: Subsequences

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

theorem :: KURATO_2:44
  for T being non empty 1-sorted,
      S being SetSequence of the carrier of T holds
    S is subsequence of S;

theorem :: KURATO_2:45
  for T being non empty 1-sorted,
      S being SetSequence of T,
      S1 being subsequence of S holds
    rng S1 c= rng S;

theorem :: KURATO_2:46
  for T being non empty 1-sorted,
      S1 being SetSequence of the carrier of T,
      S2 being subsequence of S1,
      S3 being subsequence of S2 holds
    S3 is subsequence of S1;

theorem :: KURATO_2:47
  for T being non empty 1-sorted,
      F, G being SetSequence of the carrier of T,
      A being Subset of T st
    G is subsequence of F &
    for i being Nat holds F.i = A holds G = F;

theorem :: KURATO_2:48
  for T being non empty 1-sorted,
      A being constant SetSequence of T,
      B being subsequence of A holds
   A = B;

theorem :: KURATO_2:49
  for T being non empty 1-sorted,
      S being SetSequence of the carrier of T,
      R being subsequence of S,
      n being Nat holds
    ex m being Nat st m >= n & R.n = S.m;

definition let T be non empty 1-sorted,
               X be constant SetSequence of T;
  cluster -> constant subsequence of X;
end;

scheme SubSeqChoice
  { T() -> non empty TopSpace,
    S() -> SetSequence of the carrier 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 st n <= m & P[S().m];

begin :: Lower Topological Limit

definition let T be non empty TopSpace;
           let S be SetSequence of the carrier of T;
  func Lim_inf S -> Subset of T means
:: KURATO_2:def 11
    for p being Point of T holds
        p in it iff
     for G being a_neighborhood of p
      ex k being Nat st
     for m being Nat st m > k holds S.m meets G;
end;

theorem :: KURATO_2:50
   for S being SetSequence of the carrier of TOP-REAL n,
       p being Point of TOP-REAL n,
       p' being Point of Euclid n st p = p' holds
    p in Lim_inf S iff
     for r being real number st r > 0
      ex k being Nat st
     for m being Nat st m > k holds S.m meets Ball (p', r);

theorem :: KURATO_2:51
  for T being non empty TopSpace,
      S being SetSequence of the carrier of T holds
    Cl Lim_inf S = Lim_inf S;

theorem :: KURATO_2:52
  for T being non empty TopSpace,
      S being SetSequence of the carrier of T holds
    Lim_inf S is closed;

theorem :: KURATO_2:53
  for T being non empty TopSpace,
      R, S being SetSequence of the carrier of T st
    R is subsequence of S holds Lim_inf S c= Lim_inf R;

theorem :: KURATO_2:54
  for T being non empty TopSpace,
      A, B being SetSequence of the carrier of T st
    for i being Nat holds A.i c= B.i holds
      Lim_inf A c= Lim_inf B;

theorem :: KURATO_2:55
  for T being non empty TopSpace,
      A, B, C being SetSequence of the carrier of T st
    for i being Nat holds C.i = A.i \/ B.i holds
      Lim_inf A \/ Lim_inf B c= Lim_inf C;

theorem :: KURATO_2:56
  for T being non empty TopSpace,
      A, B, C being SetSequence of the carrier of T st
    for i being Nat holds C.i = A.i /\ B.i holds
      Lim_inf C c= Lim_inf A /\ Lim_inf B;

theorem :: KURATO_2:57
  for T being non empty TopSpace,
      F, G being SetSequence of the carrier of T st
    for i being Nat holds G.i = Cl (F.i) holds
      Lim_inf G = Lim_inf F;

theorem :: KURATO_2:58
  for S being SetSequence of the carrier of TOP-REAL n,
      p being Point of TOP-REAL n holds
     (ex s being Real_Sequence of n st s is convergent &
      (for x being Nat holds s.x in S.x) & p = lim s) implies
    p in Lim_inf S;

theorem :: KURATO_2:59
   for T being non empty TopSpace,
       P being Subset of T,
       s being SetSequence of the carrier of T st
   (for i being Nat holds s.i c= P) holds
   Lim_inf s c= Cl P;

theorem :: KURATO_2:60
  for T being non empty TopSpace,
      F being SetSequence of the carrier of T,
      A being Subset of T st
    for i being Nat holds F.i = A holds Lim_inf F = Cl A;

theorem :: KURATO_2:61
  for T being non empty TopSpace,
      F being SetSequence of the carrier of T,
      A being closed Subset of T st
    for i being Nat holds F.i = A holds Lim_inf F = A;

theorem :: KURATO_2:62
  for S being SetSequence of the carrier of TOP-REAL n,
      P being Subset of TOP-REAL n st P is Bounded &
   (for i being Nat holds S.i c= P) holds
  Lim_inf S is Bounded;

theorem :: KURATO_2:63
  for S being SetSequence of the carrier of TOP-REAL 2,
      P being Subset of TOP-REAL 2 st
     P is Bounded &
    (for i being Nat holds S.i c= P) &
   for i being Nat holds S.i is compact holds
    Lim_inf S is compact;

theorem :: KURATO_2:64
  for A, B being SetSequence of the carrier of TOP-REAL n,
      C being SetSequence of the carrier of [: TOP-REAL n, TOP-REAL n :] st
    for i being Nat holds C.i = [:A.i, B.i:] holds
      [: Lim_inf A, Lim_inf B :] = Lim_inf C;

theorem :: KURATO_2:65
  for S being SetSequence of TOP-REAL 2 holds
    lim_inf S c= Lim_inf S;

theorem :: KURATO_2:66
  for C being Simple_closed_curve,
      i being Nat holds
    Fr (UBD L~Cage (C,i))` = L~Cage (C,i);

begin :: Upper Topological Limit

definition let T be non empty TopSpace;
           let S be SetSequence of the carrier of T;
  func Lim_sup S -> Subset of T means
:: KURATO_2:def 12
    for x being set holds
      x in it iff ex A being subsequence of S st x in Lim_inf A;
end;

theorem :: KURATO_2:67
  for N being Nat,
      F being sequence of TOP-REAL N,
      x being Point of TOP-REAL N,
      x' being Point of Euclid N st x = x' holds
    x is_a_cluster_point_of F iff
  for r being real number,
      n being Nat st r > 0 holds
    ex m being Nat st n <= m & F.m in Ball (x', r);

theorem :: KURATO_2:68
  for T being non empty TopSpace,
      A being SetSequence of the carrier of T holds
    Lim_inf A c= Lim_sup A;

theorem :: KURATO_2:69
  for A, B, C being SetSequence of the carrier of TOP-REAL 2 st
    (for i being Nat holds A.i c= B.i) &
     C is subsequence of A holds
     ex D being subsequence of B st for i being Nat holds C.i c= D.i;

theorem :: KURATO_2:70
  for A, B, C being SetSequence of the carrier of TOP-REAL 2 st
    (for i being Nat holds A.i c= B.i) &
     C is subsequence of B holds
     ex D being subsequence of A st for i being Nat holds D.i c= C.i;

theorem :: KURATO_2:71  :: (2)
  for A, B being SetSequence of the carrier of TOP-REAL 2 st
    for i being Nat holds A.i c= B.i holds
      Lim_sup A c= Lim_sup B;

theorem :: KURATO_2:72 :: (3)
  for A, B, C being SetSequence of the carrier of TOP-REAL 2 st
    for i being Nat holds C.i = A.i \/ B.i holds
      Lim_sup A \/ Lim_sup B c= Lim_sup C;

theorem :: KURATO_2:73 :: (4)
  for A, B, C being SetSequence of the carrier of TOP-REAL 2 st
    for i being Nat holds C.i = A.i /\ B.i holds
      Lim_sup C c= Lim_sup A /\ Lim_sup B;

theorem :: KURATO_2:74
  for A, B being SetSequence of the carrier of TOP-REAL 2,
      C, C1 being SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :] st
    (for i being Nat holds C.i = [: A.i, B.i :]) &
    C1 is subsequence of C holds
      ex A1, B1 being SetSequence of the carrier of TOP-REAL 2 st
    A1 is subsequence of A & B1 is subsequence of B &
      for i being Nat holds C1.i = [: A1.i, B1.i :];

theorem :: KURATO_2:75
  for A, B being SetSequence of the carrier of TOP-REAL 2,
      C being SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :] st
    for i being Nat holds C.i = [: A.i, B.i :] holds
      Lim_sup C c= [: Lim_sup A, Lim_sup B :];

theorem :: KURATO_2:76
  for T being non empty TopSpace,
      F being SetSequence of the carrier of T,
      A being Subset of T st
    for i being Nat holds F.i = A holds Lim_inf F = Lim_sup F;

theorem :: KURATO_2:77
  for F being SetSequence of the carrier of TOP-REAL 2,
      A being Subset of TOP-REAL 2 st
    for i being Nat holds F.i = A holds Lim_sup F = Cl A;

theorem :: KURATO_2:78
  for F, G being SetSequence of the carrier of TOP-REAL 2 st
    for i being Nat holds G.i = Cl (F.i) holds
      Lim_sup G = Lim_sup F;


Back to top