:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
begin
definition
let
T
be
1-sorted
;
mode
SetSequence of
T
is
SetSequence
of the
carrier
of
T
;
end;
begin
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
Element
of
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
Th2
:
:: KURATO_2:2
for
n
being
Element
of
NAT
for
p
being
Point
of
(
Euclid
n
)
for
x
,
p9
being
Point
of
(
TOP-REAL
n
)
for
r
being
real
number
st
p
=
p9
&
x
in
Ball
(
p
,
r
) holds
|.
(
x
-
p9
)
.|
<
r
proof
end;
theorem
Th3
:
:: KURATO_2:3
for
n
being
Element
of
NAT
for
p
being
Point
of
(
Euclid
n
)
for
x
,
p9
being
Point
of
(
TOP-REAL
n
)
for
r
being
real
number
st
p
=
p9
&
|.
(
x
-
p9
)
.|
<
r
holds
x
in
Ball
(
p
,
r
)
proof
end;
theorem
:: KURATO_2:4
for
n
being
Element
of
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
Element
of
NAT
;
cluster
TOP-REAL
n
->
first-countable
;
coherence
TOP-REAL
n
is
first-countable
proof
end;
end;
theorem
:: KURATO_2:6
for
n
being
Element
of
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
number
st
r
>
0
holds
Ball
(
p9
,
r
)
meets
A
)
proof
end;
theorem
:: KURATO_2:7
for
n
being
Element
of
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
Element
of
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
Element
of
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
Th10
:
:: KURATO_2:10
for
n
being
Element
of
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
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;
begin
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
Element
of
NAT
ex
m
being
Element
of
NAT
st
(
m
>=
n
&
R
.
n
=
S
.
m
)
proof
end;
begin
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
Element
of
NAT
st
for
m
being
Element
of
NAT
st
m
>
k
holds
S
.
m
meets
G
);
existence
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
Element
of
NAT
st
for
m
being
Element
of
NAT
st
m
>
k
holds
S
.
m
meets
G
)
proof
end;
uniqueness
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
Element
of
NAT
st
for
m
being
Element
of
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
Element
of
NAT
st
for
m
being
Element
of
NAT
st
m
>
k
holds
S
.
m
meets
G
) ) holds
b
1
=
b
2
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
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
Element
of
NAT
st
for
m
being
Element
of
NAT
st
m
>
k
holds
S
.
m
meets
G
) );
theorem
Th14
:
:: KURATO_2:14
for
n
being
Element
of
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
number
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
m
being
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
NAT
holds
G
.
i
=
Cl
(
F
.
i
)
) holds
Lim_inf
G
=
Lim_inf
F
proof
end;
theorem
:: KURATO_2:21
for
n
being
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
NAT
holds
S
.
i
c=
P
) holds
Lim_inf
S
is
compact
by
Th25
,
TOPREAL6:79
;
theorem
Th27
:
:: KURATO_2:27
for
n
being
Element
of
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
Element
of
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
Element
of
NAT
holds
Fr
(
(
UBD
(
L~
(
Cage
(
C
,
i
)
)
)
)
`
)
=
L~
(
Cage
(
C
,
i
)
)
proof
end;
begin
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
set
holds
(
x
in
it
iff ex
A
being
subsequence
of
S
st
x
in
Lim_inf
A
);
existence
ex
b
1
being
Subset
of
T
st
for
x
being
set
holds
(
x
in
b
1
iff ex
A
being
subsequence
of
S
st
x
in
Lim_inf
A
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
T
st ( for
x
being
set
holds
(
x
in
b
1
iff ex
A
being
subsequence
of
S
st
x
in
Lim_inf
A
) ) & ( for
x
being
set
holds
(
x
in
b
2
iff ex
A
being
subsequence
of
S
st
x
in
Lim_inf
A
) ) holds
b
1
=
b
2
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
3
being
Subset
of
T
holds
(
b
3
=
Lim_sup
S
iff for
x
being
set
holds
(
x
in
b
3
iff ex
A
being
subsequence
of
S
st
x
in
Lim_inf
A
) );
theorem
:: KURATO_2:30
for
N
being
Element
of
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
number
for
n
being
Element
of
NAT
st
r
>
0
holds
ex
m
being
Element
of
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
Element
of
NAT
holds
A
.
i
c=
B
.
i
) &
C
is
subsequence
of
A
holds
ex
D
being
subsequence
of
B
st
for
i
being
Element
of
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
Element
of
NAT
holds
A
.
i
c=
B
.
i
) &
C
is
subsequence
of
B
holds
ex
D
being
subsequence
of
A
st
for
i
being
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
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
Element
of
NAT
holds
G
.
i
=
Cl
(
F
.
i
)
) holds
Lim_sup
G
=
Lim_sup
F
proof
end;