:: On the {K}uratowski Limit Operators I
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
begin
theorem
:: KURATO_0:1
for
F
being
Function
for
i
being
set
st
i
in
dom
F
holds
meet
F
c=
F
.
i
proof
end;
theorem
:: KURATO_0:2
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
Function-like
V33
(
NAT
,
bool
X
)
->
non
empty
for
Element
of
bool
[:
NAT
,
(
bool
X
)
:]
;
coherence
for
b
1
being
SetSequence
of
X
holds not
b
1
is
empty
;
end;
registration
let
T
be non
empty
set
;
cluster
non
empty
Relation-like
non-empty
NAT
-defined
bool
T
-valued
Function-like
V29
(
NAT
)
V33
(
NAT
,
bool
T
) for
Element
of
bool
[:
NAT
,
(
bool
T
)
:]
;
existence
ex
b
1
being
SetSequence
of
T
st
b
1
is
non-empty
proof
end;
end;
definition
let
X
be
set
;
let
F
be
SetSequence
of
X
;
:: original:
Union
redefine
func
Union
F
->
Subset
of
X
;
coherence
Union
F
is
Subset
of
X
proof
end;
:: original:
meet
redefine
func
meet
F
->
Subset
of
X
;
coherence
meet
F
is
Subset
of
X
proof
end;
end;
begin
definition
let
X
be
set
;
let
F
be
SetSequence
of
X
;
func
lim_inf
F
->
Subset
of
X
means
:
Def1
:
:: KURATO_0:def 1
ex
f
being
SetSequence
of
X
st
(
it
=
Union
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
meet
(
F
^\
n
)
) );
existence
ex
b
1
being
Subset
of
X
ex
f
being
SetSequence
of
X
st
(
b
1
=
Union
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
meet
(
F
^\
n
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
X
st ex
f
being
SetSequence
of
X
st
(
b
1
=
Union
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
meet
(
F
^\
n
)
) ) & ex
f
being
SetSequence
of
X
st
(
b
2
=
Union
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
meet
(
F
^\
n
)
) ) holds
b
1
=
b
2
proof
end;
func
lim_sup
F
->
Subset
of
X
means
:
Def2
:
:: KURATO_0:def 2
ex
f
being
SetSequence
of
X
st
(
it
=
meet
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
Union
(
F
^\
n
)
) );
existence
ex
b
1
being
Subset
of
X
ex
f
being
SetSequence
of
X
st
(
b
1
=
meet
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
Union
(
F
^\
n
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
X
st ex
f
being
SetSequence
of
X
st
(
b
1
=
meet
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
Union
(
F
^\
n
)
) ) & ex
f
being
SetSequence
of
X
st
(
b
2
=
meet
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
Union
(
F
^\
n
)
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
lim_inf
KURATO_0:def 1 :
for
X
being
set
for
F
being
SetSequence
of
X
for
b
3
being
Subset
of
X
holds
(
b
3
=
lim_inf
F
iff ex
f
being
SetSequence
of
X
st
(
b
3
=
Union
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
meet
(
F
^\
n
)
) ) );
::
deftheorem
Def2
defines
lim_sup
KURATO_0:def 2 :
for
X
being
set
for
F
being
SetSequence
of
X
for
b
3
being
Subset
of
X
holds
(
b
3
=
lim_sup
F
iff ex
f
being
SetSequence
of
X
st
(
b
3
=
meet
f
& ( for
n
being
Element
of
NAT
holds
f
.
n
=
Union
(
F
^\
n
)
) ) );
theorem
Th3
:
:: KURATO_0:3
for
X
being
set
for
F
being
SetSequence
of
X
for
x
being
set
holds
(
x
in
meet
F
iff for
z
being
Element
of
NAT
holds
x
in
F
.
z
)
proof
end;
theorem
Th4
:
:: KURATO_0:4
for
X
being
set
for
F
being
SetSequence
of
X
for
x
being
set
holds
(
x
in
lim_inf
F
iff ex
n
being
Element
of
NAT
st
for
k
being
Element
of
NAT
holds
x
in
F
.
(
n
+
k
)
)
proof
end;
theorem
Th5
:
:: KURATO_0:5
for
X
being
set
for
F
being
SetSequence
of
X
for
x
being
set
holds
(
x
in
lim_sup
F
iff for
n
being
Element
of
NAT
ex
k
being
Element
of
NAT
st
x
in
F
.
(
n
+
k
)
)
proof
end;
theorem
:: KURATO_0:6
for
X
being
set
for
F
being
SetSequence
of
X
holds
lim_inf
F
c=
lim_sup
F
proof
end;
theorem
Th7
:
:: KURATO_0:7
for
X
being
set
for
F
being
SetSequence
of
X
holds
meet
F
c=
lim_inf
F
proof
end;
theorem
Th8
:
:: KURATO_0:8
for
X
being
set
for
F
being
SetSequence
of
X
holds
lim_sup
F
c=
Union
F
proof
end;
theorem
:: KURATO_0:9
for
X
being
set
for
F
being
SetSequence
of
X
holds
lim_inf
F
=
(
lim_sup
(
Complement
F
)
)
`
proof
end;
theorem
:: KURATO_0:10
for
X
being
set
for
A
,
B
,
C
being
SetSequence
of
X
st ( for
n
being
Element
of
NAT
holds
C
.
n
=
(
A
.
n
)
/\
(
B
.
n
)
) holds
lim_inf
C
=
(
lim_inf
A
)
/\
(
lim_inf
B
)
proof
end;
theorem
:: KURATO_0:11
for
X
being
set
for
A
,
B
,
C
being
SetSequence
of
X
st ( for
n
being
Element
of
NAT
holds
C
.
n
=
(
A
.
n
)
\/
(
B
.
n
)
) holds
lim_sup
C
=
(
lim_sup
A
)
\/
(
lim_sup
B
)
proof
end;
theorem
:: KURATO_0:12
for
X
being
set
for
A
,
B
,
C
being
SetSequence
of
X
st ( for
n
being
Element
of
NAT
holds
C
.
n
=
(
A
.
n
)
\/
(
B
.
n
)
) holds
(
lim_inf
A
)
\/
(
lim_inf
B
)
c=
lim_inf
C
proof
end;
theorem
:: KURATO_0:13
for
X
being
set
for
A
,
B
,
C
being
SetSequence
of
X
st ( for
n
being
Element
of
NAT
holds
C
.
n
=
(
A
.
n
)
/\
(
B
.
n
)
) holds
lim_sup
C
c=
(
lim_sup
A
)
/\
(
lim_sup
B
)
proof
end;
theorem
Th14
:
:: KURATO_0:14
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
Th15
:
:: KURATO_0:15
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_0:16
for
X
being
set
for
A
,
B
being
SetSequence
of
X
for
C
being
Subset
of
X
st ( for
n
being
Element
of
NAT
holds
B
.
n
=
C
\+\
(
A
.
n
)
) holds
C
\+\
(
lim_inf
A
)
c=
lim_sup
B
proof
end;
theorem
:: KURATO_0:17
for
X
being
set
for
A
,
B
being
SetSequence
of
X
for
C
being
Subset
of
X
st ( for
n
being
Element
of
NAT
holds
B
.
n
=
C
\+\
(
A
.
n
)
) holds
C
\+\
(
lim_sup
A
)
c=
lim_sup
B
proof
end;
begin
theorem
Th18
:
:: KURATO_0:18
for
f
being
Function
st ( for
i
being
Element
of
NAT
holds
f
.
(
i
+
1
)
c=
f
.
i
) holds
for
i
,
j
being
Element
of
NAT
st
i
<=
j
holds
f
.
j
c=
f
.
i
proof
end;
definition
let
T
be
set
;
let
S
be
SetSequence
of
T
;
:: original:
non-ascending
redefine
attr
S
is
non-ascending
means
:
Def3
:
:: KURATO_0:def 3
for
i
being
Element
of
NAT
holds
S
.
(
i
+
1
)
c=
S
.
i
;
compatibility
(
S
is
non-ascending
iff for
i
being
Element
of
NAT
holds
S
.
(
i
+
1
)
c=
S
.
i
)
proof
end;
:: original:
non-descending
redefine
attr
S
is
non-descending
means
:
Def4
:
:: KURATO_0:def 4
for
i
being
Element
of
NAT
holds
S
.
i
c=
S
.
(
i
+
1
)
;
compatibility
(
S
is
non-descending
iff for
i
being
Element
of
NAT
holds
S
.
i
c=
S
.
(
i
+
1
)
)
proof
end;
end;
::
deftheorem
Def3
defines
non-ascending
KURATO_0:def 3 :
for
T
being
set
for
S
being
SetSequence
of
T
holds
(
S
is
non-ascending
iff for
i
being
Element
of
NAT
holds
S
.
(
i
+
1
)
c=
S
.
i
);
::
deftheorem
Def4
defines
non-descending
KURATO_0:def 4 :
for
T
being
set
for
S
being
SetSequence
of
T
holds
(
S
is
non-descending
iff for
i
being
Element
of
NAT
holds
S
.
i
c=
S
.
(
i
+
1
)
);
theorem
Th19
:
:: KURATO_0:19
for
T
being
set
for
F
being
SetSequence
of
T
for
x
being
set
st
F
is
V50
() & ex
k
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
n
>
k
holds
x
in
F
.
n
holds
x
in
meet
F
proof
end;
theorem
:: KURATO_0:20
for
T
being
set
for
F
being
SetSequence
of
T
st
F
is
V50
() holds
lim_inf
F
=
meet
F
proof
end;
theorem
:: KURATO_0:21
for
T
being
set
for
F
being
SetSequence
of
T
st
F
is
V51
() holds
lim_sup
F
=
Union
F
proof
end;
begin
definition
let
T
be
set
;
let
S
be
SetSequence
of
T
;
attr
S
is
convergent
means
:
Def5
:
:: KURATO_0:def 5
lim_sup
S
=
lim_inf
S
;
end;
::
deftheorem
Def5
defines
convergent
KURATO_0:def 5 :
for
T
being
set
for
S
being
SetSequence
of
T
holds
(
S
is
convergent
iff
lim_sup
S
=
lim_inf
S
);
theorem
:: KURATO_0:22
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;
registration
let
T
be
set
;
cluster
Function-like
constant
V33
(
NAT
,
bool
T
)
->
V50
()
V51
()
convergent
for
Element
of
bool
[:
NAT
,
(
bool
T
)
:]
;
coherence
for
b
1
being
SetSequence
of
T
st
b
1
is
constant
holds
(
b
1
is
convergent
&
b
1
is
V51
() &
b
1
is
V50
() )
proof
end;
end;
registration
let
T
be
set
;
cluster
non
empty
Relation-like
NAT
-defined
bool
T
-valued
Function-like
constant
V29
(
NAT
)
V33
(
NAT
,
bool
T
) for
Element
of
bool
[:
NAT
,
(
bool
T
)
:]
;
existence
ex
b
1
being
SetSequence
of
T
st
(
b
1
is
constant
& not
b
1
is
empty
)
proof
end;
end;
notation
let
T
be
set
;
let
S
be
convergent
SetSequence
of
T
;
synonym
Lim_K
S
for
lim_sup
S
;
end;
theorem
:: KURATO_0:23
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
Element
of
NAT
st
for
k
being
Element
of
NAT
holds
x
in
F
.
(
n
+
k
)
)
proof
end;