:: KURATO_2 semantic presentation

theorem Th1: :: KURATO_2:1

for b₁, b₂ being set
for b₃ being Subset of b₁ st not b₂ in b₃ & b₂ in b₁ holds
b₂ in b₃ `

proof end;

theorem Th2: :: KURATO_2:2

for b₁ being Function
for b₂ being set st b₂ in dom b₁ holds
meet b₁ c= b₁ . b₂

proof end;

theorem Th3: :: KURATO_2:3

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds
( b₂ = b₃ iff for b₄ being Nat holds b₂ . b₄ = b₃ . b₄ )

proof end;

theorem Th4: :: KURATO_2:4

for b₁, b₂, b₃, b₄ being set st b₁ meets b₂ & b₃ meets b₄ holds
[:b₁,b₃:] meets [:b₂,b₄:]

proof end;

registration

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

end;

registration

let c₁ be non empty set ;
cluster non-empty M6( NAT , bool a₁);
existence

proof end;

end;

definition

let c₁ be 1-sorted ;
mode SetSequence of a₁ is SetSequence of the carrier of a₁;

end;

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

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

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine func Union as Union c₂ -> Subset of a₁;
coherence

proof end;

redefine func meet as meet c₂ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Function of NAT ,c₁;
let c₃ be Nat;
canceled;
func c₂ ^\ c₃ -> Function of NAT ,a₁ means :Def2: :: KURATO_2:def 2
for b₁ being Nat holds a₄ . b₁ = a₂ . (b₁ + a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 KURATO_2:def 1 :

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

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func lim_inf c₂ -> Subset of a₁ means :Def3: :: KURATO_2:def 3
ex b₁ being SetSequence of a₁ st
( a₃ = Union b₁ & ( for b₂ being Nat holds b₁ . b₂ = meet (a₂ ^\ b₂) ) );
existence

proof end;

uniqueness

proof end;

func lim_sup c₂ -> Subset of a₁ means :Def4: :: KURATO_2:def 4
ex b₁ being SetSequence of a₁ st
( a₃ = meet b₁ & ( for b₂ being Nat holds b₁ . b₂ = Union (a₂ ^\ b₂) ) );
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 Th5: :: KURATO_2:5

canceled;

theorem Th6: :: KURATO_2:6

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being set holds
( b₃ in meet b₂ iff for b₄ being Nat holds b₃ in b₂ . b₄ )

proof end;

theorem Th7: :: KURATO_2:7

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being set holds
( b₃ in lim_inf b₂ iff ex b₄ being Nat st
for b₅ being Nat holds b₃ in b₂ . (b₄ + b₅) )

proof end;

theorem Th8: :: KURATO_2:8

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being set holds
( b₃ in lim_sup b₂ iff for b₄ being Nat ex b₅ being Nat st b₃ in b₂ . (b₄ + b₅) )

proof end;

theorem Th9: :: KURATO_2:9

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_inf b₂ c= lim_sup b₂

proof end;

theorem Th10: :: KURATO_2:10

for b₁ being set
for b₂ being SetSequence of b₁ holds meet b₂ c= lim_inf b₂

proof end;

theorem Th11: :: KURATO_2:11

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_sup b₂ c= Union b₂

proof end;

theorem Th12: :: KURATO_2:12

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_inf b₂ = (lim_sup (Complement b₂)) `

proof end;

theorem Th13: :: KURATO_2:13

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) /\ (b₃ . b₅) ) holds
lim_inf b₄ = (lim_inf b₂) /\ (lim_inf b₃)

proof end;

theorem Th14: :: KURATO_2:14

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) \/ (b₃ . b₅) ) holds
lim_sup b₄ = (lim_sup b₂) \/ (lim_sup b₃)

proof end;

theorem Th15: :: KURATO_2:15

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) \/ (b₃ . b₅) ) holds
(lim_inf b₂) \/ (lim_inf b₃) c= lim_inf b₄

proof end;

theorem Th16: :: KURATO_2:16

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) /\ (b₃ . b₅) ) holds
lim_sup b₄ c= (lim_sup b₂) /\ (lim_sup b₃)

proof end;

theorem Th17: :: KURATO_2:17

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being Subset of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
lim_sup b₂ = b₃

proof end;

theorem Th18: :: KURATO_2:18

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being Subset of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
lim_inf b₂ = b₃

proof end;

theorem Th19: :: KURATO_2:19

for b₁ being set
for b₂, b₃ being SetSequence of b₁
for b₄ being Subset of b₁ st ( for b₅ being Nat holds b₃ . b₅ = b₄ \+\ (b₂ . b₅) ) holds
b₄ \+\ (lim_inf b₂) c= lim_sup b₃

proof end;

theorem Th20: :: KURATO_2:20

for b₁ being set
for b₂, b₃ being SetSequence of b₁
for b₄ being Subset of b₁ st ( for b₅ being Nat holds b₃ . b₅ = b₄ \+\ (b₂ . b₅) ) holds
b₄ \+\ (lim_sup b₂) c= lim_sup b₃

proof end;

definition

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

end;

:: deftheorem Def5 defines descending KURATO_2:def 5 :

:: deftheorem Def6 defines ascending KURATO_2:def 6 :

theorem Th21: :: KURATO_2:21

for b₁ being Function st ( for b₂ being Nat holds b₁ . (b₂ + 1) c= b₁ . b₂ ) holds
for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ c= b₁ . b₂

proof end;

theorem Th22: :: KURATO_2:22

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is descending holds
for b₃, b₄ being Nat st b₃ >= b₄ holds
b₂ . b₃ c= b₂ . b₄

proof end;

theorem Th23: :: KURATO_2:23

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is ascending holds
for b₃, b₄ being Nat st b₃ >= b₄ holds
b₂ . b₄ c= b₂ . b₃

proof end;

theorem Th24: :: KURATO_2:24

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being set st b₂ is descending & ex b₄ being Nat st
for b₅ being Nat st b₅ > b₄ holds
b₃ in b₂ . b₅ holds
b₃ in meet b₂

proof end;

theorem Th25: :: KURATO_2:25

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is descending holds
lim_inf b₂ = meet b₂

proof end;

theorem Th26: :: KURATO_2:26

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is ascending holds
lim_sup b₂ = Union b₂

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
attr a₂ is convergent means :Def7: :: KURATO_2:def 7
lim_sup a₂ = lim_inf a₂;

end;

:: deftheorem Def7 defines convergent KURATO_2:def 7 :

theorem Th27: :: KURATO_2:27

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is constant holds
the_value_of b₂ is Subset of b₁

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine attr constant as a₂ is constant means :Def8: :: KURATO_2:def 8
ex b₁ being Subset of a₁ st
for b₂ being Nat holds a₂ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def8 defines constant KURATO_2:def 8 :

registration

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

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be set ;
let c₂ be convergent SetSequence of c₁;
func Lim_K c₂ -> Subset of a₁ means :Def9: :: KURATO_2:def 9
( a₃ = lim_sup a₂ & a₃ = lim_inf a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines Lim_K KURATO_2:def 9 :

theorem Th28: :: KURATO_2:28

for b₁ being set
for b₂ being convergent SetSequence of b₁
for b₃ being set holds
( b₃ in Lim_K b₂ iff ex b₄ being Nat st
for b₅ being Nat holds b₃ in b₂ . (b₄ + b₅) )

proof end;

registration

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

end;

theorem Th29: :: KURATO_2:29

canceled;

theorem Th30: :: KURATO_2:30

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being real number holds Ball b₂,b₃ is open Subset of (TOP-REAL b₁)

proof end;

theorem Th31: :: KURATO_2:31

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Point of (Euclid b₁) st b₂ = b₄ & b₃ = b₅ holds
dist b₄,b₅ = |.(b₂ - b₃).|

proof end;

theorem Th32: :: KURATO_2:32

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being real number st b₂ = b₄ & b₃ in Ball b₂,b₅ holds
|.(b₃ - b₄).| < b₅

proof end;

theorem Th33: :: KURATO_2:33

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being real number st b₂ = b₄ & |.(b₃ - b₄).| < b₅ holds
b₃ in Ball b₂,b₅

proof end;

theorem Th34: :: KURATO_2:34

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₂ in Cl b₃ holds
ex b₄ being Real_Sequence of b₁ st
( rng b₄ c= b₃ & b₄ is convergent & lim b₄ = b₂ )

proof end;

registration

let c₁ be non empty MetrSpace;
cluster TopSpaceMetr a₁ -> first-countable ;
coherence by FRECHET:21;

end;

registration

let c₁ be Nat;
cluster TOP-REAL a₁ -> first-countable ;
coherence ;

end;

theorem Th35: :: KURATO_2:35

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being real number st b₂ = b₃ & b₄ > 0 holds
Ball b₂,b₄ is a_neighborhood of b₃

proof end;

theorem Th36: :: KURATO_2:36

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
( b₃ in Cl b₂ iff for b₅ being real number st b₅ > 0 holds
Ball b₄,b₅ meets b₂ )

proof end;

theorem Th37: :: KURATO_2:37

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₄ = b₂ & b₂ <> b₃ holds
ex b₅ being Real st not b₃ in Ball b₄,b₅

proof end;

theorem Th38: :: KURATO_2:38

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds
( not b₂ is Bounded iff for b₃ being Real st b₃ > 0 holds
ex b₄, b₅ being Point of (Euclid b₁) st
( b₄ in b₂ & b₅ in b₂ & dist b₄,b₅ > b₃ ) )

proof end;

theorem Th39: :: KURATO_2:39

for b₁ being Nat
for b₂, b₃ being real number
for b₄, b₅ being Point of (Euclid b₁) st Ball b₄,b₂ meets Ball b₅,b₃ holds
dist b₄,b₅ < b₂ + b₃

proof end;

theorem Th40: :: KURATO_2:40

for b₁ being Nat
for b₂, b₃, b₄ being real number
for b₅, b₆, b₇ being Point of (Euclid b₁) st Ball b₅,b₂ meets Ball b₇,b₄ & Ball b₇,b₄ meets Ball b₆,b₃ holds
dist b₅,b₆ < (b₂ + b₃) + (2 * b₄)

proof end;

theorem Th41: :: KURATO_2:41

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being Subset of [:b₁,b₂:] holds
( b₅ is a_neighborhood of [:{b₃},{b₄}:] iff b₅ is a_neighborhood of [b₃,b₄] )

proof end;

definition

let c₁ be non empty set ;
let c₂ be SetSequence of c₁;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Subset of a₁;
coherence

proof end;

end;

theorem Th42: :: KURATO_2:42

for b₁ being non empty 1-sorted
for b₂ being SetSequence of the carrier of b₁
for b₃ being Seq_of_Nat holds b₂ * b₃ is SetSequence of b₁

proof end;

theorem Th43: :: KURATO_2:43

id NAT is increasing Seq_of_Nat

proof end;

registration

cluster id NAT -> real-yielding ;
coherence ;

end;

Lemma35: for b₁ being non empty 1-sorted
for b₂ being SetSequence of the carrier of b₁ ex b₃ being increasing Seq_of_Nat st b₂ = b₂ * b₃

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be SetSequence of the carrier of c₁;
mode subsequence of c₂ -> SetSequence of a₁ means :Def10: :: KURATO_2:def 10
ex b₁ being increasing Seq_of_Nat st a₃ = a₂ * b₁;
existence

proof end;

end;

:: deftheorem Def10 defines subsequence KURATO_2:def 10 :

theorem Th44: :: KURATO_2:44

for b₁ being non empty 1-sorted
for b₂ being SetSequence of the carrier of b₁ holds b₂ is subsequence of b₂

proof end;

theorem Th45: :: KURATO_2:45

for b₁ being non empty 1-sorted
for b₂ being SetSequence of b₁
for b₃ being subsequence of b₂ holds rng b₃ c= rng b₂

proof end;

theorem Th46: :: KURATO_2:46

for b₁ being non empty 1-sorted
for b₂ being SetSequence of the carrier of b₁
for b₃ being subsequence of b₂
for b₄ being subsequence of b₃ holds b₄ is subsequence of b₂

proof end;

theorem Th47: :: KURATO_2:47

for b₁ being non empty 1-sorted
for b₂, b₃ being SetSequence of the carrier of b₁
for b₄ being Subset of b₁ st b₃ is subsequence of b₂ & ( for b₅ being Nat holds b₂ . b₅ = b₄ ) holds
b₃ = b₂

proof end;

theorem Th48: :: KURATO_2:48

for b₁ being non empty 1-sorted
for b₂ being V152 SetSequence of b₁
for b₃ being subsequence of b₂ holds b₂ = b₃

proof end;

theorem Th49: :: KURATO_2:49

for b₁ being non empty 1-sorted
for b₂ being SetSequence of the carrier of b₁
for b₃ being subsequence of b₂
for b₄ being Nat ex b₅ being Nat st
( b₅ >= b₄ & b₃ . b₄ = b₂ . b₅ )

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be V152 SetSequence of c₁;
cluster -> V152 subsequence of a₂;
coherence

proof end;

end;

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

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

provided

E40: for b₁ being Nat ex b₂ being Nat st
( b₁ <= b₂ & P₁[F₂() . b₂] )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SetSequence of the carrier of c₁;
func Lim_inf c₂ -> Subset of a₁ means :Def11: :: KURATO_2:def 11
for b₁ being Point of a₁ holds
( b₁ in a₃ iff for b₂ being a_neighborhood of b₁ ex b₃ being Nat st
for b₄ being Nat st b₄ > b₃ holds
a₂ . b₄ meets b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Lim_inf KURATO_2:def 11 :

theorem Th50: :: KURATO_2:50

for b₁ being Nat
for b₂ being SetSequence of the carrier of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
( b₃ in Lim_inf b₂ iff for b₅ being real number st b₅ > 0 holds
ex b₆ being Nat st
for b₇ being Nat st b₇ > b₆ holds
b₂ . b₇ meets Ball b₄,b₅ )

proof end;

theorem Th51: :: KURATO_2:51

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁ holds Cl (Lim_inf b₂) = Lim_inf b₂

proof end;

theorem Th52: :: KURATO_2:52

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁ holds Lim_inf b₂ is closed

proof end;

theorem Th53: :: KURATO_2:53

for b₁ being non empty TopSpace
for b₂, b₃ being SetSequence of the carrier of b₁ st b₂ is subsequence of b₃ holds
Lim_inf b₃ c= Lim_inf b₂

proof end;

theorem Th54: :: KURATO_2:54

for b₁ being non empty TopSpace
for b₂, b₃ being SetSequence of the carrier of b₁ st ( for b₄ being Nat holds b₂ . b₄ c= b₃ . b₄ ) holds
Lim_inf b₂ c= Lim_inf b₃

proof end;

theorem Th55: :: KURATO_2:55

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being SetSequence of the carrier of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) \/ (b₃ . b₅) ) holds
(Lim_inf b₂) \/ (Lim_inf b₃) c= Lim_inf b₄

proof end;

theorem Th56: :: KURATO_2:56

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being SetSequence of the carrier of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (b₂ . b₅) /\ (b₃ . b₅) ) holds
Lim_inf b₄ c= (Lim_inf b₂) /\ (Lim_inf b₃)

proof end;

theorem Th57: :: KURATO_2:57

for b₁ being non empty TopSpace
for b₂, b₃ being SetSequence of the carrier of b₁ st ( for b₄ being Nat holds b₃ . b₄ = Cl (b₂ . b₄) ) holds
Lim_inf b₃ = Lim_inf b₂

proof end;

theorem Th58: :: KURATO_2:58

for b₁ being Nat
for b₂ being SetSequence of the carrier of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) st ex b₄ being Real_Sequence of b₁ st
( b₄ is convergent & ( for b₅ being Nat holds b₄ . b₅ in b₂ . b₅ ) & b₃ = lim b₄ ) holds
b₃ in Lim_inf b₂

proof end;

theorem Th59: :: KURATO_2:59

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being SetSequence of the carrier of b₁ st ( for b₄ being Nat holds b₃ . b₄ c= b₂ ) holds
Lim_inf b₃ c= Cl b₂

proof end;

theorem Th60: :: KURATO_2:60

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁
for b₃ being Subset of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
Lim_inf b₂ = Cl b₃

proof end;

theorem Th61: :: KURATO_2:61

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁
for b₃ being closed Subset of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
Lim_inf b₂ = b₃

proof end;

theorem Th62: :: KURATO_2:62

for b₁ being Nat
for b₂ being SetSequence of the carrier of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₃ is Bounded & ( for b₄ being Nat holds b₂ . b₄ c= b₃ ) holds
Lim_inf b₂ is Bounded

proof end;

theorem Th63: :: KURATO_2:63

for b₁ being SetSequence of the carrier of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₂ is Bounded & ( for b₃ being Nat holds b₁ . b₃ c= b₂ ) holds
Lim_inf b₁ is compact

proof end;

theorem Th64: :: KURATO_2:64

for b₁ being Nat
for b₂, b₃ being SetSequence of the carrier of (TOP-REAL b₁)
for b₄ being SetSequence of the carrier of [:(TOP-REAL b₁),(TOP-REAL b₁):] st ( for b₅ being Nat holds b₄ . b₅ = [:(b₂ . b₅),(b₃ . b₅):] ) holds
[:(Lim_inf b₂),(Lim_inf b₃):] = Lim_inf b₄

proof end;

theorem Th65: :: KURATO_2:65

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

proof end;

theorem Th66: :: KURATO_2:66

for b₁ being Simple_closed_curve
for b₂ being Nat holds Fr ((UBD (L~ (Cage b₁,b₂))) ` ) = L~ (Cage b₁,b₂)

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SetSequence of the carrier of c₁;
func Lim_sup c₂ -> Subset of a₁ means :Def12: :: KURATO_2:def 12
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being subsequence of a₂ st b₁ in Lim_inf b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Lim_sup KURATO_2:def 12 :

theorem Th67: :: KURATO_2:67

for b₁ being Nat
for b₂ being sequence of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
( b₃ is_a_cluster_point_of b₂ iff for b₅ being real number
for b₆ being Nat st b₅ > 0 holds
ex b₇ being Nat st
( b₆ <= b₇ & b₂ . b₇ in Ball b₄,b₅ ) )

proof end;

theorem Th68: :: KURATO_2:68

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁ holds Lim_inf b₂ c= Lim_sup b₂

proof end;

theorem Th69: :: KURATO_2:69

for b₁, b₂, b₃ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₄ being Nat holds b₁ . b₄ c= b₂ . b₄ ) & b₃ is subsequence of b₁ holds
ex b₄ being subsequence of b₂ st
for b₅ being Nat holds b₃ . b₅ c= b₄ . b₅

proof end;

theorem Th70: :: KURATO_2:70

for b₁, b₂, b₃ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₄ being Nat holds b₁ . b₄ c= b₂ . b₄ ) & b₃ is subsequence of b₂ holds
ex b₄ being subsequence of b₁ st
for b₅ being Nat holds b₄ . b₅ c= b₃ . b₅

proof end;

theorem Th71: :: KURATO_2:71

for b₁, b₂ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₃ being Nat holds b₁ . b₃ c= b₂ . b₃ ) holds
Lim_sup b₁ c= Lim_sup b₂

proof end;

theorem Th72: :: KURATO_2:72

for b₁, b₂, b₃ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₄ being Nat holds b₃ . b₄ = (b₁ . b₄) \/ (b₂ . b₄) ) holds
(Lim_sup b₁) \/ (Lim_sup b₂) c= Lim_sup b₃

proof end;

theorem Th73: :: KURATO_2:73

for b₁, b₂, b₃ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₄ being Nat holds b₃ . b₄ = (b₁ . b₄) /\ (b₂ . b₄) ) holds
Lim_sup b₃ c= (Lim_sup b₁) /\ (Lim_sup b₂)

proof end;

theorem Th74: :: KURATO_2:74

for b₁, b₂ being SetSequence of the carrier of (TOP-REAL 2)
for b₃, b₄ being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b₅ being Nat holds b₃ . b₅ = [:(b₁ . b₅),(b₂ . b₅):] ) & b₄ is subsequence of b₃ holds
ex b₅, b₆ being SetSequence of the carrier of (TOP-REAL 2) st
( b₅ is subsequence of b₁ & b₆ is subsequence of b₂ & ( for b₇ being Nat holds b₄ . b₇ = [:(b₅ . b₇),(b₆ . b₇):] ) )

proof end;

theorem Th75: :: KURATO_2:75

for b₁, b₂ being SetSequence of the carrier of (TOP-REAL 2)
for b₃ being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b₄ being Nat holds b₃ . b₄ = [:(b₁ . b₄),(b₂ . b₄):] ) holds
Lim_sup b₃ c= [:(Lim_sup b₁),(Lim_sup b₂):]

proof end;

theorem Th76: :: KURATO_2:76

for b₁ being non empty TopSpace
for b₂ being SetSequence of the carrier of b₁
for b₃ being Subset of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
Lim_inf b₂ = Lim_sup b₂

proof end;

theorem Th77: :: KURATO_2:77

for b₁ being SetSequence of the carrier of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st ( for b₃ being Nat holds b₁ . b₃ = b₂ ) holds
Lim_sup b₁ = Cl b₂

proof end;

theorem Th78: :: KURATO_2:78

for b₁, b₂ being SetSequence of the carrier of (TOP-REAL 2) st ( for b₃ being Nat holds b₂ . b₃ = Cl (b₁ . b₃) ) holds
Lim_sup b₂ = Lim_sup b₁

proof end;