:: by Adam Grabowski

::

:: Received August 12, 2003

:: Copyright (c) 2003-2018 Association of Mizar Users

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;

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

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)

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 )

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
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 )

( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable )

proof 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 )

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)

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 ) )

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

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)

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] )

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

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 )

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;

ex b_{1} being Subset of T st

for p being Point of T holds

( p in b_{1} 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 b_{1}, b_{2} being Subset of T st ( for p being Point of T holds

( p in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 );

ex b

for p being Point of T holds

( p in b

for m being Nat st m > k holds

S . m meets G )

proof end;

uniqueness for b

( p in b

for m being Nat st m > k holds

S . m meets G ) ) & ( for p being Point of T holds

( p in b

for m being Nat st m > k holds

S . m meets G ) ) holds

b

proof 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_{3} being Subset of T holds

( b_{3} = Lim_inf S iff for p being Point of T holds

( p in b_{3} 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 T being non empty TopSpace

for S being SetSequence of the carrier of T

for b

( b

( p in b

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) )

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

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;

coherence

Lim_inf S is closed

end;
let S be SetSequence of the carrier of T;

coherence

Lim_inf S is closed

proof 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

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

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

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)

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

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

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

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

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

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

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

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

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:29

for C being Simple_closed_curve

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

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;

ex b_{1} being Subset of T st

for x being object holds

( x in b_{1} iff ex A being subsequence of S st x in Lim_inf A )

for b_{1}, b_{2} being Subset of T st ( for x being object holds

( x in b_{1} iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being object holds

( x in b_{2} iff ex A being subsequence of S st x in Lim_inf A ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff ex A being subsequence of S st x in Lim_inf A );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof 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_{3} being Subset of T holds

( b_{3} = Lim_sup S iff for x being object holds

( x in b_{3} iff ex A being subsequence of S st x in Lim_inf A ) );

for T being non empty TopSpace

for S being SetSequence of the carrier of T

for b

( b

( x in b

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) ) )

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

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

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

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

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

(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)

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):] ) )

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):]

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

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

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

Lim_sup G = Lim_sup F

proof end;