:: Heine--Borel's Covering Theorem
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991 Association of Mizar Users
begin
theorem
Th1
:
:: HEINE:1
for
x
,
y
being
real
number
for
A
being
SubSpace
of
RealSpace
for
p
,
q
being
Point
of
A
st
x
=
p
&
y
=
q
holds
dist
p
,
q
=
abs
(
x
-
y
)
proof
end;
theorem
:: HEINE:2
canceled;
theorem
:: HEINE:3
canceled;
theorem
:: HEINE:4
canceled;
theorem
:: HEINE:5
canceled;
theorem
Th6
:
:: HEINE:6
for
n
being
Element
of
NAT
for
seq
being
Real_Sequence
st
seq
is
increasing
&
rng
seq
c=
NAT
holds
n
<=
seq
.
n
proof
end;
definition
let
seq
be
Real_Sequence
;
let
k
be
Element
of
NAT
;
func
k
to_power
seq
->
Real_Sequence
means
:
Def1
:
:: HEINE:def 1
for
n
being
Element
of
NAT
holds
it
.
n
=
k
to_power
(
seq
.
n
)
;
existence
ex
b
1
being
Real_Sequence
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
k
to_power
(
seq
.
n
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
k
to_power
(
seq
.
n
)
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
k
to_power
(
seq
.
n
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
to_power
HEINE:def 1 :
for
seq
being
Real_Sequence
for
k
being
Element
of
NAT
for
b
3
being
Real_Sequence
holds
(
b
3
=
k
to_power
seq
iff for
n
being
Element
of
NAT
holds
b
3
.
n
=
k
to_power
(
seq
.
n
)
);
theorem
:: HEINE:7
canceled;
theorem
:: HEINE:8
canceled;
theorem
Th9
:
:: HEINE:9
for
seq
being
Real_Sequence
st
seq
is
divergent_to+infty
holds
2
to_power
seq
is
divergent_to+infty
proof
end;
theorem
:: HEINE:10
canceled;
theorem
:: HEINE:11
for
a
,
b
being
real
number
st
a
<=
b
holds
Closed-Interval-TSpace
a
,
b
is
compact
proof
end;