:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition

let T be 1-sorted ;
mode SetSequence of T is SetSequence of the carrier of T;

end;

registration

let f be FinSequence of the carrier of (TOP-REAL 2);

cluster L~ f -> closed ;

coherence
L~ f is closed ;

end;

theorem Th1: :: KURATO_2:1

for n being Nat
for x being Point of (Euclid n)
for r being Real holds Ball (x,r) is open Subset of (TOP-REAL n) by TOPREAL3:8, GOBOARD6:3;

theorem Th2: :: KURATO_2:2

for n being Nat
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r

proof end;

theorem Th3: :: KURATO_2:3

for n being Nat
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being Real st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)

proof end;

theorem :: KURATO_2:4

for n being Nat
for r being Point of (TOP-REAL n)
for 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 )

proof end;

registration

let M be non empty MetrSpace;

cluster TopSpaceMetr M -> first-countable ;

coherence
TopSpaceMetr M is first-countable by FRECHET:20;

end;

Lm1: for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )

proof end;

theorem Th5: :: KURATO_2:5

for T being non empty TopSpace holds
( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable )

proof end;

registration

let n be Nat;

cluster TOP-REAL n -> first-countable ;

coherence
TOP-REAL n is first-countable

proof end;

end;

theorem :: KURATO_2:6

for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )

proof end;

theorem :: KURATO_2:7

for n being Nat
for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)

proof end;

theorem Th8: :: KURATO_2:8

for n being Nat
for S being Subset of (TOP-REAL n) holds
( not S is 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 ) )

proof end;

theorem Th9: :: KURATO_2:9

for n being Nat
for a, b being Real
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b

proof end;

theorem Th10: :: KURATO_2:10

for n being Nat
for a, b, c being Real
for 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)

proof end;

theorem Th11: :: KURATO_2:11

for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )

proof end;

theorem Th12: :: KURATO_2:12

for T being non empty 1-sorted
for F, G being SetSequence of the carrier of T
for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F

proof end;

theorem :: KURATO_2:13

for T being non empty 1-sorted
for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Nat ex m being Element of NAT st
( m >= n & R . n = S . m )

proof end;

definition

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;

func Lim_inf S -> Subset of T means :Def1: :: KURATO_2:def 1
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 );

existence
ex b₁ being Subset of T st
for p being Point of T holds
( p in b₁ 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 )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for p being Point of T holds
( p in b₁ 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 ) ) & ( for p being Point of T holds
( p in b₂ 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 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Lim_inf KURATO_2:def 1 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_inf S iff for p being Point of T holds
( p in b₃ 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 ) );

theorem Th14: :: KURATO_2:14

for n being Nat
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r) )

proof end;

theorem Th15: :: KURATO_2:15

for T being non empty TopSpace
for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S

proof end;

registration

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;

cluster Lim_inf S -> closed ;

coherence
Lim_inf S is closed

proof end;

end;

theorem :: KURATO_2:16

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

proof end;

theorem Th17: :: KURATO_2:17

for T being non empty TopSpace
for 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

proof end;

theorem :: KURATO_2:18

for T being non empty TopSpace
for 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

proof end;

theorem :: KURATO_2:19

for T being non empty TopSpace
for 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)

proof end;

theorem Th20: :: KURATO_2:20

for T being non empty TopSpace
for 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

proof end;

theorem :: KURATO_2:21

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

proof end;

theorem Th22: :: KURATO_2:22

for T being non empty TopSpace
for P being Subset of T
for 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

proof end;

theorem Th23: :: KURATO_2:23

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Cl A

proof end;

theorem :: KURATO_2:24

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A

proof end;

theorem Th25: :: KURATO_2:25

for n being Nat
for S being SetSequence of the carrier of (TOP-REAL n)
for 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

proof end;

theorem :: KURATO_2:26

for S being SetSequence of the carrier of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is compact by Th25, TOPREAL6:79;

theorem Th27: :: KURATO_2:27

for n being Nat
for A, B being SetSequence of the carrier of (TOP-REAL n)
for 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

proof end;

theorem :: KURATO_2:28

for S being SetSequence of (TOP-REAL 2) holds lim_inf S c= Lim_inf S

proof end;

theorem :: KURATO_2:29

for C being Simple_closed_curve
for i being Nat holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))

proof end;

definition

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;

func Lim_sup S -> Subset of T means :Def2: :: KURATO_2:def 2
for x being object holds
( x in it iff ex A being subsequence of S st x in Lim_inf A );

existence
ex b₁ being Subset of T st
for x being object holds
( x in b₁ iff ex A being subsequence of S st x in Lim_inf A )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for x being object holds
( x in b₁ iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being object holds
( x in b₂ iff ex A being subsequence of S st x in Lim_inf A ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Lim_sup KURATO_2:def 2 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_sup S iff for x being object holds
( x in b₃ iff ex A being subsequence of S st x in Lim_inf A ) );

theorem :: KURATO_2:30

for N being Nat
for F being sequence of (TOP-REAL N)
for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )

proof end;

theorem Th31: :: KURATO_2:31

for T being non empty TopSpace
for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A

proof end;

theorem Th32: :: KURATO_2:32

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

proof end;

theorem :: KURATO_2:33

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

proof end;

theorem Th34: :: KURATO_2:34

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

proof end;

theorem :: KURATO_2:35

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

proof end;

theorem :: KURATO_2:36

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)

proof end;

theorem Th37: :: KURATO_2:37

for A, B being SetSequence of the carrier of (TOP-REAL 2)
for 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):] ) )

proof end;

theorem :: KURATO_2:38

for A, B being SetSequence of the carrier of (TOP-REAL 2)
for 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):]

proof end;

:: Kuratowski convergence

theorem Th39: :: KURATO_2:39

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F

proof end;

theorem :: KURATO_2:40

for F being SetSequence of the carrier of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A

proof end;

theorem :: KURATO_2:41

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

proof end;