:: Metric Spaces as Topological Spaces - Fundamental Concepts
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-2015 Association of Mizar Users
:: Topological spaces
theorem
:: TOPMETR:1
for
T
being
TopStruct
for
F
being
Subset-Family
of
T
holds
(
F
is
Cover
of
T
iff the
carrier
of
T
c=
union
F
)
by
SETFAM_1:def 11
;
theorem
:: TOPMETR:2
for
T
being non
empty
TopSpace
for
A
being non
empty
SubSpace
of
T
st
T
is
T_2
holds
A
is
T_2
proof
end;
theorem
Th3
:
:: TOPMETR:3
for
T
being
TopSpace
for
A
,
B
being
SubSpace
of
T
st the
carrier
of
A
c=
the
carrier
of
B
holds
A
is
SubSpace
of
B
proof
end;
theorem
Th4
:
:: TOPMETR:4
for
T
being non
empty
TopSpace
for
P
,
Q
being
Subset
of
T
holds
(
T
|
P
is
SubSpace
of
T
|
(
P
\/
Q
)
&
T
|
Q
is
SubSpace
of
T
|
(
P
\/
Q
)
)
proof
end;
theorem
:: TOPMETR:5
for
T
being non
empty
TopSpace
for
p
being
Point
of
T
for
P
being non
empty
Subset
of
T
st
p
in
P
holds
for
Q
being
a_neighborhood
of
p
for
p9
being
Point
of
(
T
|
P
)
for
Q9
being
Subset
of
(
T
|
P
)
st
Q9
=
Q
/\
P
&
p9
=
p
holds
Q9
is
a_neighborhood
of
p9
proof
end;
theorem
:: TOPMETR:6
for
A
,
B
being
TopSpace
for
f
being
Function
of
A
,
B
for
C
being
Subset
of
B
st
f
is
continuous
holds
for
h
being
Function
of
A
,
(
B
|
C
)
st
h
=
f
holds
h
is
continuous
proof
end;
theorem
:: TOPMETR:7
for
X
being
TopStruct
for
Y
being non
empty
TopStruct
for
K0
being
Subset
of
X
for
f
being
Function
of
X
,
Y
for
g
being
Function
of
(
X
|
K0
)
,
Y
st
f
is
continuous
&
g
=
f
|
K0
holds
g
is
continuous
proof
end;
Lm1
:
for
M
being
MetrSpace
holds
MetrStruct
(# the
carrier
of
M
, the
distance
of
M
#) is
MetrSpace
proof
end;
definition
let
M
be
MetrSpace
;
mode
SubSpace
of
M
->
MetrSpace
means
:
Def1
:
:: TOPMETR:def 1
( the
carrier
of
it
c=
the
carrier
of
M
& ( for
x
,
y
being
Point
of
it
holds the
distance
of
it
.
(
x
,
y
)
=
the
distance
of
M
.
(
x
,
y
) ) );
existence
ex
b
1
being
MetrSpace
st
( the
carrier
of
b
1
c=
the
carrier
of
M
& ( for
x
,
y
being
Point
of
b
1
holds the
distance
of
b
1
.
(
x
,
y
)
=
the
distance
of
M
.
(
x
,
y
) ) )
proof
end;
end;
::
deftheorem
Def1
defines
SubSpace
TOPMETR:def 1 :
for
M
,
b
2
being
MetrSpace
holds
(
b
2
is
SubSpace
of
M
iff ( the
carrier
of
b
2
c=
the
carrier
of
M
& ( for
x
,
y
being
Point
of
b
2
holds the
distance
of
b
2
.
(
x
,
y
)
=
the
distance
of
M
.
(
x
,
y
) ) ) );
registration
let
M
be
MetrSpace
;
cluster
strict
Reflexive
discerning
V122
()
triangle
for
SubSpace
of
M
;
existence
ex
b
1
being
SubSpace
of
M
st
b
1
is
strict
proof
end;
end;
registration
let
M
be non
empty
MetrSpace
;
cluster
non
empty
strict
Reflexive
discerning
V122
()
triangle
for
SubSpace
of
M
;
existence
ex
b
1
being
SubSpace
of
M
st
(
b
1
is
strict
& not
b
1
is
empty
)
proof
end;
end;
theorem
Th8
:
:: TOPMETR:8
for
M
being non
empty
MetrSpace
for
A
being non
empty
SubSpace
of
M
for
p
being
Point
of
A
holds
p
is
Point
of
M
proof
end;
theorem
Th9
:
:: TOPMETR:9
for
r
being
Real
for
M
being
MetrSpace
for
A
being
SubSpace
of
M
for
x
being
Point
of
M
for
x9
being
Point
of
A
st
x
=
x9
holds
Ball
(
x9
,
r
)
=
(
Ball
(
x
,
r
)
)
/\
the
carrier
of
A
proof
end;
definition
let
M
be non
empty
MetrSpace
;
let
A
be non
empty
Subset
of
M
;
func
M
|
A
->
strict
SubSpace
of
M
means
:
Def2
:
:: TOPMETR:def 2
the
carrier
of
it
=
A
;
existence
ex
b
1
being
strict
SubSpace
of
M
st the
carrier
of
b
1
=
A
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
SubSpace
of
M
st the
carrier
of
b
1
=
A
& the
carrier
of
b
2
=
A
holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
|
TOPMETR:def 2 :
for
M
being non
empty
MetrSpace
for
A
being non
empty
Subset
of
M
for
b
3
being
strict
SubSpace
of
M
holds
(
b
3
=
M
|
A
iff the
carrier
of
b
3
=
A
);
registration
let
M
be non
empty
MetrSpace
;
let
A
be non
empty
Subset
of
M
;
cluster
M
|
A
->
non
empty
strict
;
coherence
not
M
|
A
is
empty
by
Def2
;
end;
definition
let
a
,
b
be
Real
;
assume
A1
:
a
<=
b
;
func
Closed-Interval-MSpace
(
a
,
b
)
->
non
empty
strict
SubSpace
of
RealSpace
means
:
Def3
:
:: TOPMETR:def 3
for
P
being non
empty
Subset
of
RealSpace
st
P
=
[.
a
,
b
.]
holds
it
=
RealSpace
|
P
;
existence
ex
b
1
being non
empty
strict
SubSpace
of
RealSpace
st
for
P
being non
empty
Subset
of
RealSpace
st
P
=
[.
a
,
b
.]
holds
b
1
=
RealSpace
|
P
proof
end;
uniqueness
for
b
1
,
b
2
being non
empty
strict
SubSpace
of
RealSpace
st ( for
P
being non
empty
Subset
of
RealSpace
st
P
=
[.
a
,
b
.]
holds
b
1
=
RealSpace
|
P
) & ( for
P
being non
empty
Subset
of
RealSpace
st
P
=
[.
a
,
b
.]
holds
b
2
=
RealSpace
|
P
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
Closed-Interval-MSpace
TOPMETR:def 3 :
for
a
,
b
being
Real
st
a
<=
b
holds
for
b
3
being non
empty
strict
SubSpace
of
RealSpace
holds
(
b
3
=
Closed-Interval-MSpace
(
a
,
b
) iff for
P
being non
empty
Subset
of
RealSpace
st
P
=
[.
a
,
b
.]
holds
b
3
=
RealSpace
|
P
);
theorem
Th10
:
:: TOPMETR:10
for
a
,
b
being
Real
st
a
<=
b
holds
the
carrier
of
(
Closed-Interval-MSpace
(
a
,
b
)
)
=
[.
a
,
b
.]
proof
end;
definition
let
M
be
MetrStruct
;
let
F
be
Subset-Family
of
M
;
attr
F
is
being_ball-family
means
:: TOPMETR:def 4
for
P
being
set
st
P
in
F
holds
ex
p
being
Point
of
M
ex
r
being
Real
st
P
=
Ball
(
p
,
r
);
end;
::
deftheorem
defines
being_ball-family
TOPMETR:def 4 :
for
M
being
MetrStruct
for
F
being
Subset-Family
of
M
holds
(
F
is
being_ball-family
iff for
P
being
set
st
P
in
F
holds
ex
p
being
Point
of
M
ex
r
being
Real
st
P
=
Ball
(
p
,
r
) );
theorem
Th11
:
:: TOPMETR:11
for
p
,
q
being
Point
of
RealSpace
for
x
,
y
being
Real
st
x
=
p
&
y
=
q
holds
dist
(
p
,
q
)
=
|.
(
x
-
y
)
.|
by
METRIC_1:def 12
;
:: Metric spaces and topology
theorem
:: TOPMETR:12
for
M
being
MetrStruct
holds
( the
carrier
of
M
=
the
carrier
of
(
TopSpaceMetr
M
)
& the
topology
of
(
TopSpaceMetr
M
)
=
Family_open_set
M
) ;
theorem
Th13
:
:: TOPMETR:13
for
M
being non
empty
MetrSpace
for
A
being non
empty
SubSpace
of
M
holds
TopSpaceMetr
A
is
SubSpace
of
TopSpaceMetr
M
proof
end;
theorem
Th14
:
:: TOPMETR:14
for
r
being
Real
for
M
being
triangle
MetrStruct
for
p
being
Point
of
M
for
P
being
Subset
of
(
TopSpaceMetr
M
)
st
P
=
Ball
(
p
,
r
) holds
P
is
open
by
PCOMPS_1:29
;
theorem
Th15
:
:: TOPMETR:15
for
M
being non
empty
MetrSpace
for
P
being
Subset
of
(
TopSpaceMetr
M
)
holds
(
P
is
open
iff for
p
being
Point
of
M
st
p
in
P
holds
ex
r
being
Real
st
(
r
>
0
&
Ball
(
p
,
r
)
c=
P
) )
by
PCOMPS_1:def 4
;
definition
let
M
be
MetrStruct
;
attr
M
is
compact
means
:: TOPMETR:def 5
TopSpaceMetr
M
is
compact
;
end;
::
deftheorem
defines
compact
TOPMETR:def 5 :
for
M
being
MetrStruct
holds
(
M
is
compact
iff
TopSpaceMetr
M
is
compact
);
theorem
:: TOPMETR:16
for
M
being non
empty
MetrSpace
holds
(
M
is
compact
iff for
F
being
Subset-Family
of
M
st
F
is
being_ball-family
&
F
is
Cover
of
M
holds
ex
G
being
Subset-Family
of
M
st
(
G
c=
F
&
G
is
Cover
of
M
&
G
is
finite
) )
proof
end;
:: REAL as topological space
definition
func
R^1
->
TopSpace
equals
:: TOPMETR:def 6
TopSpaceMetr
RealSpace
;
correctness
coherence
TopSpaceMetr
RealSpace
is
TopSpace
;
;
end;
::
deftheorem
defines
R^1
TOPMETR:def 6 :
R^1
=
TopSpaceMetr
RealSpace
;
registration
cluster
R^1
->
non
empty
strict
;
coherence
(
R^1
is
strict
& not
R^1
is
empty
)
;
end;
theorem
:: TOPMETR:17
the
carrier
of
R^1
=
REAL
;
definition
let
a
,
b
be
Real
;
func
Closed-Interval-TSpace
(
a
,
b
)
->
non
empty
strict
SubSpace
of
R^1
equals
:: TOPMETR:def 7
TopSpaceMetr
(
Closed-Interval-MSpace
(
a
,
b
)
)
;
coherence
TopSpaceMetr
(
Closed-Interval-MSpace
(
a
,
b
)
)
is non
empty
strict
SubSpace
of
R^1
by
Th13
;
end;
::
deftheorem
defines
Closed-Interval-TSpace
TOPMETR:def 7 :
for
a
,
b
being
Real
holds
Closed-Interval-TSpace
(
a
,
b
)
=
TopSpaceMetr
(
Closed-Interval-MSpace
(
a
,
b
)
)
;
theorem
Th18
:
:: TOPMETR:18
for
a
,
b
being
Real
st
a
<=
b
holds
the
carrier
of
(
Closed-Interval-TSpace
(
a
,
b
)
)
=
[.
a
,
b
.]
by
Th10
;
theorem
Th19
:
:: TOPMETR:19
for
a
,
b
being
Real
st
a
<=
b
holds
for
P
being
Subset
of
R^1
st
P
=
[.
a
,
b
.]
holds
Closed-Interval-TSpace
(
a
,
b
)
=
R^1
|
P
proof
end;
theorem
Th20
:
:: TOPMETR:20
Closed-Interval-TSpace
(
0
,1)
=
I[01]
proof
end;
definition
:: original:
I[01]
redefine
func
I[01]
->
SubSpace
of
R^1
;
coherence
I[01]
is
SubSpace
of
R^1
by
Th20
;
end;
Lm2
:
for
a
,
b
,
r
being
Real
st
r
>=
0
&
a
+
r
<=
b
holds
a
<=
b
proof
end;
theorem
:: TOPMETR:21
for
f
being
Function
of
R^1
,
R^1
st ex
a
,
b
being
Real
st
for
x
being
Real
holds
f
.
x
=
(
a
*
x
)
+
b
holds
f
is
continuous
proof
end;
::Moved from JORDAN16:6, AK 20.02.2006
theorem
:: TOPMETR:22
for
T
being non
empty
TopSpace
for
A
,
B
being
Subset
of
T
st
A
c=
B
holds
T
|
A
is
SubSpace
of
T
|
B
proof
end;
::Moved from JGRAPH_5:6,7, AK 20.02.2006
theorem
Th23
:
:: TOPMETR:23
for
a
,
b
,
d
,
e
being
Real
for
B
being
Subset
of
(
Closed-Interval-TSpace
(
d
,
e
)
)
st
d
<=
a
&
a
<=
b
&
b
<=
e
&
B
=
[.
a
,
b
.]
holds
Closed-Interval-TSpace
(
a
,
b
)
=
(
Closed-Interval-TSpace
(
d
,
e
)
)
|
B
proof
end;
theorem
:: TOPMETR:24
for
a
,
b
being
Real
for
B
being
Subset
of
I[01]
st
0
<=
a
&
a
<=
b
&
b
<=
1 &
B
=
[.
a
,
b
.]
holds
Closed-Interval-TSpace
(
a
,
b
)
=
I[01]
|
B
by
Th20
,
Th23
;
:: from BORSUK_6, 2007.04.08, A,T.
definition
let
T
be
1-sorted
;
attr
T
is
real-membered
means
:
Def8
:
:: TOPMETR:def 8
the
carrier
of
T
is
real-membered
;
end;
::
deftheorem
Def8
defines
real-membered
TOPMETR:def 8 :
for
T
being
1-sorted
holds
(
T
is
real-membered
iff the
carrier
of
T
is
real-membered
);
registration
cluster
I[01]
->
real-membered
;
coherence
I[01]
is
real-membered
by
BORSUK_1:40
;
end;
:: from RCOMP_3, 2007.04.08, A,T.
registration
cluster
non
empty
real-membered
for
1-sorted
;
existence
ex
b
1
being
1-sorted
st
( not
b
1
is
empty
&
b
1
is
real-membered
)
proof
end;
end;
registration
let
S
be
real-membered
1-sorted
;
cluster
the
carrier
of
S
->
real-membered
;
coherence
the
carrier
of
S
is
real-membered
by
Def8
;
end;
:: from BORSUK_6, 2010.03.07, A.T.
registration
cluster
R^1
->
real-membered
;
coherence
R^1
is
real-membered
;
end;
:: from BORSUK_6, 2010.05.31, A.K.
registration
cluster
non
empty
strict
TopSpace-like
real-membered
for
TopStruct
;
existence
ex
b
1
being
TopSpace
st
(
b
1
is
strict
& not
b
1
is
empty
&
b
1
is
real-membered
)
proof
end;
end;
registration
let
T
be
real-membered
TopStruct
;
cluster
->
real-membered
for
SubSpace
of
T
;
coherence
for
b
1
being
SubSpace
of
T
holds
b
1
is
real-membered
proof
end;
end;
:: from EUCLID_9, 2010.10.05, A.K.
registration
cluster
RealSpace
->
real-membered
;
coherence
RealSpace
is
real-membered
;
end;