:: KURATO_2 semantic presentation

theorem Th1: :: KURATO_2:1

for X, x being set
for A being Subset of X st not x in A & x in X holds
x in A `

proof end;

theorem :: KURATO_2:2

for F being Function
for i being set st i in dom F holds
meet F c= F . i

proof end;

theorem Th3: :: KURATO_2:3

for T being set
for S1, S2 being SetSequence of T holds
( S1 = S2 iff for n being Nat holds S1 . n = S2 . n )

proof end;

theorem Th4: :: KURATO_2:4

for A, B, C, D being set st A meets B & C meets D holds
[:A,C:] meets [:B,D:]

proof end;

registration

let X be set ;
cluster -> non empty M6( NAT , bool X);
coherence ;

end;

registration

let T be non empty set ;
cluster non-empty M6( NAT , bool T);
existence

proof end;

end;

definition

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

end;

scheme :: KURATO_2:sch 1
LambdaSSeq{ F₁() -> set , F₂( set ) -> Subset of F₁() } :

ex f being SetSequence of F₁() st
for n being Nat holds f . n = F₂(n)

proof end;

definition

let X be set ;
let F be SetSequence of X;
:: original: Union
redefine func Union F -> Subset of X;
coherence

proof end;

:: original: meet
redefine func meet F -> Subset of X;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem KURATO_2:def 1 :

:: deftheorem Def2 defines ^\ KURATO_2:def 2 :

definition

let X be set ;
let F be SetSequence of X;
func lim_inf F -> Subset of X means :Def3: :: KURATO_2:def 3
ex f being SetSequence of X st
( it = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) );
existence

proof end;

uniqueness

proof end;

func lim_sup F -> Subset of X means :Def4: :: KURATO_2:def 4
ex f being SetSequence of X st
( it = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines lim_inf KURATO_2:def 3 :

:: deftheorem Def4 defines lim_sup KURATO_2:def 4 :

theorem :: KURATO_2:5

canceled;

theorem Th6: :: KURATO_2:6

for X being set
for F being SetSequence of X
for x being set holds
( x in meet F iff for z being Nat holds x in F . z )

proof end;

theorem Th7: :: KURATO_2:7

for X being set
for F being SetSequence of X
for 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) )

proof end;

theorem Th8: :: KURATO_2:8

for X being set
for F being SetSequence of X
for x being set holds
( x in lim_sup F iff for n being Nat ex k being Nat st x in F . (n + k) )

proof end;

theorem :: KURATO_2:9

for X being set
for F being SetSequence of X holds lim_inf F c= lim_sup F

proof end;

theorem Th10: :: KURATO_2:10

for X being set
for F being SetSequence of X holds meet F c= lim_inf F

proof end;

theorem Th11: :: KURATO_2:11

for X being set
for F being SetSequence of X holds lim_sup F c= Union F

proof end;

theorem :: KURATO_2:12

for X being set
for F being SetSequence of X holds lim_inf F = (lim_sup (Complement F)) `

proof end;

theorem :: KURATO_2:13

for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = (lim_inf A) /\ (lim_inf B)

proof end;

theorem :: KURATO_2:14

for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) \/ (B . n) ) holds
lim_sup C = (lim_sup A) \/ (lim_sup B)

proof end;

theorem :: KURATO_2:15

for X being set
for A, B, C being SetSequence 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

proof end;

theorem :: KURATO_2:16

for X being set
for A, B, C being SetSequence 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)

proof end;

theorem Th17: :: KURATO_2:17

for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B

proof end;

theorem Th18: :: KURATO_2:18

for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B

proof end;

theorem :: KURATO_2:19

for X being set
for A, B being SetSequence of X
for 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

proof end;

theorem :: KURATO_2:20

for X being set
for A, B being SetSequence of X
for 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

proof end;

definition

let T be set ;
let S be SetSequence of T;
attr S is descending means :Def5: :: KURATO_2:def 5
for i being Nat holds S . (i + 1) c= S . i;
attr S is ascending means :Def6: :: KURATO_2:def 6
for i being Nat holds S . i c= S . (i + 1);

end;

:: deftheorem Def5 defines descending KURATO_2:def 5 :

:: deftheorem Def6 defines ascending KURATO_2:def 6 :

theorem Th21: :: KURATO_2:21

for f being Function st ( for i being Nat holds f . (i + 1) c= f . i ) holds
for i, j being Nat st i <= j holds
f . j c= f . i

proof end;

theorem Th22: :: KURATO_2:22

for T being set
for C being SetSequence of T st C is descending holds
for i, m being Nat st i >= m holds
C . i c= C . m

proof end;

theorem Th23: :: KURATO_2:23

for T being set
for C being SetSequence of T st C is ascending holds
for i, m being Nat st i >= m holds
C . m c= C . i

proof end;

theorem Th24: :: KURATO_2:24

for T being set
for F being SetSequence of T
for 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

proof end;

theorem :: KURATO_2:25

for T being set
for F being SetSequence of T st F is descending holds
lim_inf F = meet F

proof end;

theorem :: KURATO_2:26

for T being set
for F being SetSequence of T st F is ascending holds
lim_sup F = Union F

proof end;

definition

let T be set ;
let S be SetSequence of T;
attr S is convergent means :Def7: :: KURATO_2:def 7
lim_sup S = lim_inf S;

end;

:: deftheorem Def7 defines convergent KURATO_2:def 7 :

theorem Th27: :: KURATO_2:27

for T being set
for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T

proof end;

definition

let T be set ;
let S be SetSequence of T;
:: original: constant
redefine attr S is constant means :Def8: :: KURATO_2:def 8
ex A being Subset of T st
for n being Nat holds S . n = A;
compatibility

proof end;

end;

:: deftheorem Def8 defines constant KURATO_2:def 8 :

registration

let T be set ;
cluster V152 -> non empty descending ascending convergent M6( NAT , bool T);
coherence

proof end;

end;

registration

let T be set ;
cluster non empty V152 descending ascending convergent M6( NAT , bool T);
existence

proof end;

end;

definition

let T be set ;
let S be convergent SetSequence of T;
func Lim_K S -> Subset of T means :Def9: :: KURATO_2:def 9
( it = lim_sup S & it = lim_inf S );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines Lim_K KURATO_2:def 9 :

theorem :: KURATO_2:28

for X being set
for F being convergent SetSequence of X
for 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) )

proof end;

registration

let f be FinSequence of the carrier of (TOP-REAL 2);
cluster L~ f -> closed ;
coherence by SPPOL_1:49;

end;

theorem :: KURATO_2:29

canceled;

theorem Th30: :: KURATO_2:30

for n being Nat
for x being Point of (Euclid n)
for r being real number holds Ball x,r is open Subset of (TOP-REAL n)

proof end;

theorem Th31: :: KURATO_2:31

for n being Nat
for p, q being Point of (TOP-REAL n)
for p', q' being Point of (Euclid n) st p = p' & q = q' holds
dist p',q' = |.(p - q).|

proof end;

theorem Th32: :: KURATO_2:32

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

proof end;

theorem Th33: :: KURATO_2:33

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

proof end;

theorem :: KURATO_2:34

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 by FRECHET:21;

end;

registration

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

end;

theorem Th35: :: KURATO_2:35

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

proof end;

theorem :: KURATO_2:36

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

proof end;

theorem :: KURATO_2:37

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

proof end;

theorem Th38: :: KURATO_2:38

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 Th39: :: KURATO_2:39

for n being Nat
for a, b being real number
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 Th40: :: KURATO_2:40

for n being Nat
for a, b, c being real number
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 Th41: :: KURATO_2:41

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;

definition

let T be non empty set ;
let S be SetSequence of T;
let i be Nat;
:: original: .
redefine func S . i -> Subset of T;
coherence

proof end;

end;

theorem Th42: :: KURATO_2:42

for T being non empty 1-sorted
for S being SetSequence of the carrier of T
for R being Seq_of_Nat holds S * R is SetSequence of T

proof end;

theorem Th43: :: KURATO_2:43

id NAT is increasing Seq_of_Nat

proof end;

registration

cluster id NAT -> real-yielding ;
coherence ;

end;

Lm1: for T being non empty 1-sorted
for S being SetSequence of the carrier of T ex NS being increasing Seq_of_Nat st S = S * NS

proof end;

definition

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

proof end;

end;

:: deftheorem Def10 defines subsequence KURATO_2:def 10 :

theorem Th44: :: KURATO_2:44

for T being non empty 1-sorted
for S being SetSequence of the carrier of T holds S is subsequence of S

proof end;

theorem :: KURATO_2:45

for T being non empty 1-sorted
for S being SetSequence of T
for S1 being subsequence of S holds rng S1 c= rng S

proof end;

theorem :: KURATO_2:46

for T being non empty 1-sorted
for S1 being SetSequence of the carrier of T
for S2 being subsequence of S1
for S3 being subsequence of S2 holds S3 is subsequence of S1

proof end;

theorem Th47: :: KURATO_2:47

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

for T being non empty 1-sorted
for A being V152 SetSequence of T
for B being subsequence of A holds A = B

proof end;

theorem Th49: :: KURATO_2:49

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 Nat st
( m >= n & R . n = S . m )

proof end;

registration

let T be non empty 1-sorted ;
let X be V152 SetSequence of T;
cluster -> V152 subsequence of X;
coherence

proof end;

end;

scheme :: KURATO_2:sch 2
SubSeqChoice{ F₁() -> non empty TopSpace, F₂() -> SetSequence of the carrier of F₁(), P₁[ set ] } :

ex S1 being subsequence of F₂() st
for n being Nat holds P₁[S1 . n]

provided

A1: for n being Nat ex m being Nat st
( n <= m & P₁[F₂() . 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 :Def11: :: 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 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Lim_inf KURATO_2:def 11 :

theorem Th50: :: KURATO_2:50

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

proof end;

theorem Th51: :: KURATO_2:51

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;

theorem Th52: :: KURATO_2:52

for T being non empty TopSpace
for S being SetSequence of the carrier of T holds Lim_inf S is closed

proof end;

theorem :: KURATO_2:53

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 Th54: :: KURATO_2:54

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

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

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 Th57: :: KURATO_2:57

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

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 Th59: :: KURATO_2:59

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 Th60: :: KURATO_2:60

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

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 Th62: :: KURATO_2:62

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

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

proof end;

theorem Th64: :: KURATO_2:64

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

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

proof end;

theorem :: KURATO_2:66

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 :Def12: :: 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 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Lim_sup KURATO_2:def 12 :

theorem :: KURATO_2:67

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

proof end;

theorem Th68: :: KURATO_2:68

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

proof end;

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

proof end;

theorem Th71: :: KURATO_2:71

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

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

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 Th74: :: KURATO_2:74

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

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;

theorem Th76: :: KURATO_2:76

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

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

proof end;