:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
definition
let
g
,
s
be
real
number
;
:: original:
[.
redefine
func
[.
g
,
s
.]
->
Subset
of
REAL
equals
:: RCOMP_1:def 1
{
r
where
r
is
Real
: (
g
<=
r
&
r
<=
s
)
}
;
coherence
[.
g
,
s
.]
is
Subset
of
REAL
proof
end;
compatibility
for
b
1
being
Subset
of
REAL
holds
(
b
1
=
[.
g
,
s
.]
iff
b
1
=
{
r
where
r
is
Real
: (
g
<=
r
&
r
<=
s
)
}
)
proof
end;
end;
::
deftheorem
defines
[.
RCOMP_1:def 1 :
for
g
,
s
being
real
number
holds
[.
g
,
s
.]
=
{
r
where
r
is
Real
: (
g
<=
r
&
r
<=
s
)
}
;
definition
let
g
,
s
be
ext-real
number
;
:: original:
].
redefine
func
].
g
,
s
.[
->
Subset
of
REAL
equals
:: RCOMP_1:def 2
{
r
where
r
is
Real
: (
g
<
r
&
r
<
s
)
}
;
coherence
].
g
,
s
.[
is
Subset
of
REAL
proof
end;
compatibility
for
b
1
being
Subset
of
REAL
holds
(
b
1
=
].
g
,
s
.[
iff
b
1
=
{
r
where
r
is
Real
: (
g
<
r
&
r
<
s
)
}
)
proof
end;
end;
::
deftheorem
defines
].
RCOMP_1:def 2 :
for
g
,
s
being
ext-real
number
holds
].
g
,
s
.[
=
{
r
where
r
is
Real
: (
g
<
r
&
r
<
s
)
}
;
theorem
Th1
:
:: RCOMP_1:1
for
r
,
p
,
g
being
real
number
holds
(
r
in
].
(
p
-
g
)
,
(
p
+
g
)
.[
iff
abs
(
r
-
p
)
<
g
)
proof
end;
theorem
:: RCOMP_1:2
for
r
,
p
,
g
being
real
number
holds
(
r
in
[.
p
,
g
.]
iff
abs
(
(
p
+
g
)
-
(
2
*
r
)
)
<=
g
-
p
)
proof
end;
theorem
:: RCOMP_1:3
for
r
,
p
,
g
being
real
number
holds
(
r
in
].
p
,
g
.[
iff
abs
(
(
p
+
g
)
-
(
2
*
r
)
)
<
g
-
p
)
proof
end;
definition
let
X
be
Subset
of
REAL
;
attr
X
is
compact
means
:
Def3
:
:: RCOMP_1:def 3
for
s1
being
Real_Sequence
st
rng
s1
c=
X
holds
ex
s2
being
Real_Sequence
st
(
s2
is
subsequence
of
s1
&
s2
is
convergent
&
lim
s2
in
X
);
end;
::
deftheorem
Def3
defines
compact
RCOMP_1:def 3 :
for
X
being
Subset
of
REAL
holds
(
X
is
compact
iff for
s1
being
Real_Sequence
st
rng
s1
c=
X
holds
ex
s2
being
Real_Sequence
st
(
s2
is
subsequence
of
s1
&
s2
is
convergent
&
lim
s2
in
X
) );
definition
let
X
be
Subset
of
REAL
;
attr
X
is
closed
means
:
Def4
:
:: RCOMP_1:def 4
for
s1
being
Real_Sequence
st
rng
s1
c=
X
&
s1
is
convergent
holds
lim
s1
in
X
;
end;
::
deftheorem
Def4
defines
closed
RCOMP_1:def 4 :
for
X
being
Subset
of
REAL
holds
(
X
is
closed
iff for
s1
being
Real_Sequence
st
rng
s1
c=
X
&
s1
is
convergent
holds
lim
s1
in
X
);
definition
let
X
be
Subset
of
REAL
;
attr
X
is
open
means
:
Def5
:
:: RCOMP_1:def 5
X
`
is
closed
;
end;
::
deftheorem
Def5
defines
open
RCOMP_1:def 5 :
for
X
being
Subset
of
REAL
holds
(
X
is
open
iff
X
`
is
closed
);
theorem
Th4
:
:: RCOMP_1:4
for
s
,
g
being
real
number
for
s1
being
Real_Sequence
st
rng
s1
c=
[.
s
,
g
.]
holds
s1
is
bounded
proof
end;
theorem
Th5
:
:: RCOMP_1:5
for
s
,
g
being
real
number
holds
[.
s
,
g
.]
is
closed
proof
end;
theorem
:: RCOMP_1:6
for
s
,
g
being
real
number
holds
[.
s
,
g
.]
is
compact
proof
end;
theorem
Th7
:
:: RCOMP_1:7
for
p
,
q
being
real
number
holds
].
p
,
q
.[
is
open
proof
end;
registration
let
p
,
q
be
real
number
;
cluster
].
p
,
q
.[
->
open
for
Subset
of
REAL
;
coherence
for
b
1
being
Subset
of
REAL
st
b
1
=
].
p
,
q
.[
holds
b
1
is
open
by
Th7
;
cluster
[.
p
,
q
.]
->
closed
for
Subset
of
REAL
;
coherence
for
b
1
being
Subset
of
REAL
st
b
1
=
[.
p
,
q
.]
holds
b
1
is
closed
by
Th5
;
end;
theorem
Th8
:
:: RCOMP_1:8
for
X
being
Subset
of
REAL
st
X
is
compact
holds
X
is
closed
proof
end;
registration
cluster
compact
->
closed
for
Element
of
K19
(
REAL
);
coherence
for
b
1
being
Subset
of
REAL
st
b
1
is
compact
holds
b
1
is
closed
by
Th8
;
end;
theorem
Th9
:
:: RCOMP_1:9
for
s1
being
Real_Sequence
for
X
being
Subset
of
REAL
st ( for
p
being
real
number
st
p
in
X
holds
ex
r
being
real
number
ex
n
being
Element
of
NAT
st
(
0
<
r
& ( for
m
being
Element
of
NAT
st
n
<
m
holds
r
<
abs
(
(
s1
.
m
)
-
p
)
) ) ) holds
for
s2
being
Real_Sequence
st
s2
is
subsequence
of
s1
&
s2
is
convergent
holds
not
lim
s2
in
X
proof
end;
theorem
Th10
:
:: RCOMP_1:10
for
X
being
Subset
of
REAL
st
X
is
compact
holds
X
is
real-bounded
proof
end;
theorem
:: RCOMP_1:11
for
X
being
Subset
of
REAL
st
X
is
real-bounded
&
X
is
closed
holds
X
is
compact
proof
end;
theorem
Th12
:
:: RCOMP_1:12
for
X
being
Subset
of
REAL
st
X
<>
{}
&
X
is
closed
&
X
is
bounded_above
holds
upper_bound
X
in
X
proof
end;
theorem
Th13
:
:: RCOMP_1:13
for
X
being
Subset
of
REAL
st
X
<>
{}
&
X
is
closed
&
X
is
bounded_below
holds
lower_bound
X
in
X
proof
end;
theorem
:: RCOMP_1:14
for
X
being
Subset
of
REAL
st
X
<>
{}
&
X
is
compact
holds
(
upper_bound
X
in
X
&
lower_bound
X
in
X
)
proof
end;
theorem
:: RCOMP_1:15
for
X
being
Subset
of
REAL
st
X
is
compact
& ( for
g1
,
g2
being
real
number
st
g1
in
X
&
g2
in
X
holds
[.
g1
,
g2
.]
c=
X
) holds
ex
p
,
g
being
real
number
st
X
=
[.
p
,
g
.]
proof
end;
registration
cluster
V50
()
V51
()
V52
()
open
for
Element
of
K19
(
REAL
);
existence
ex
b
1
being
Subset
of
REAL
st
b
1
is
open
proof
end;
end;
definition
let
r
be
real
number
;
mode
Neighbourhood
of
r
->
Subset
of
REAL
means
:
Def6
:
:: RCOMP_1:def 6
ex
g
being
real
number
st
(
0
<
g
&
it
=
].
(
r
-
g
)
,
(
r
+
g
)
.[
);
existence
ex
b
1
being
Subset
of
REAL
ex
g
being
real
number
st
(
0
<
g
&
b
1
=
].
(
r
-
g
)
,
(
r
+
g
)
.[
)
proof
end;
end;
::
deftheorem
Def6
defines
Neighbourhood
RCOMP_1:def 6 :
for
r
being
real
number
for
b
2
being
Subset
of
REAL
holds
(
b
2
is
Neighbourhood
of
r
iff ex
g
being
real
number
st
(
0
<
g
&
b
2
=
].
(
r
-
g
)
,
(
r
+
g
)
.[
) );
registration
let
r
be
real
number
;
cluster
->
open
for
Neighbourhood
of
r
;
coherence
for
b
1
being
Neighbourhood
of
r
holds
b
1
is
open
proof
end;
end;
theorem
:: RCOMP_1:16
for
r
being
real
number
for
N
being
Neighbourhood
of
r
holds
r
in
N
proof
end;
theorem
:: RCOMP_1:17
for
r
being
real
number
for
N1
,
N2
being
Neighbourhood
of
r
ex
N
being
Neighbourhood
of
r
st
(
N
c=
N1
&
N
c=
N2
)
proof
end;
theorem
Th18
:
:: RCOMP_1:18
for
X
being
open
Subset
of
REAL
for
r
being
real
number
st
r
in
X
holds
ex
N
being
Neighbourhood
of
r
st
N
c=
X
proof
end;
theorem
:: RCOMP_1:19
for
X
being
open
Subset
of
REAL
for
r
being
real
number
st
r
in
X
holds
ex
g
being
real
number
st
(
0
<
g
&
].
(
r
-
g
)
,
(
r
+
g
)
.[
c=
X
)
proof
end;
theorem
:: RCOMP_1:20
for
X
being
Subset
of
REAL
st ( for
r
being
real
number
st
r
in
X
holds
ex
N
being
Neighbourhood
of
r
st
N
c=
X
) holds
X
is
open
proof
end;
theorem
Th21
:
:: RCOMP_1:21
for
X
being
Subset
of
REAL
st
X
is
open
&
X
is
bounded_above
holds
not
upper_bound
X
in
X
proof
end;
theorem
Th22
:
:: RCOMP_1:22
for
X
being
Subset
of
REAL
st
X
is
open
&
X
is
bounded_below
holds
not
lower_bound
X
in
X
proof
end;
theorem
:: RCOMP_1:23
for
X
being
Subset
of
REAL
st
X
is
open
&
X
is
real-bounded
& ( for
g1
,
g2
being
real
number
st
g1
in
X
&
g2
in
X
holds
[.
g1
,
g2
.]
c=
X
) holds
ex
p
,
g
being
real
number
st
X
=
].
p
,
g
.[
proof
end;
:: From RCOMP_2, AG 19.12.2008
definition
let
g
be
real
number
;
let
s
be
ext-real
number
;
:: original:
[.
redefine
func
[.
g
,
s
.[
->
Subset
of
REAL
equals
:: RCOMP_1:def 7
{
r
where
r
is
Real
: (
g
<=
r
&
r
<
s
)
}
;
coherence
[.
g
,
s
.[
is
Subset
of
REAL
proof
end;
compatibility
for
b
1
being
Subset
of
REAL
holds
(
b
1
=
[.
g
,
s
.[
iff
b
1
=
{
r
where
r
is
Real
: (
g
<=
r
&
r
<
s
)
}
)
proof
end;
end;
::
deftheorem
defines
[.
RCOMP_1:def 7 :
for
g
being
real
number
for
s
being
ext-real
number
holds
[.
g
,
s
.[
=
{
r
where
r
is
Real
: (
g
<=
r
&
r
<
s
)
}
;
definition
let
g
be
ext-real
number
;
let
s
be
real
number
;
:: original:
].
redefine
func
].
g
,
s
.]
->
Subset
of
REAL
equals
:: RCOMP_1:def 8
{
r
where
r
is
Real
: (
g
<
r
&
r
<=
s
)
}
;
coherence
].
g
,
s
.]
is
Subset
of
REAL
proof
end;
compatibility
for
b
1
being
Subset
of
REAL
holds
(
b
1
=
].
g
,
s
.]
iff
b
1
=
{
r
where
r
is
Real
: (
g
<
r
&
r
<=
s
)
}
)
proof
end;
end;
::
deftheorem
defines
].
RCOMP_1:def 8 :
for
g
being
ext-real
number
for
s
being
real
number
holds
].
g
,
s
.]
=
{
r
where
r
is
Real
: (
g
<
r
&
r
<=
s
)
}
;