Database
BASIC TOPOLOGY
Metric spaces
Open sets of a metric space
tmsds
Next ⟩
tmstopn
Metamath Proof Explorer
Ascii
Unicode
Theorem
tmsds
Description:
The metric of a constructed metric space.
(Contributed by
Mario Carneiro
, 2-Sep-2015)
Ref
Expression
Hypothesis
tmsbas.k
⊢
K
=
toMetSp
⁡
D
Assertion
tmsds
⊢
D
∈
∞Met
⁡
X
→
D
=
dist
⁡
K
Proof
Step
Hyp
Ref
Expression
1
tmsbas.k
⊢
K
=
toMetSp
⁡
D
2
eqid
⊢
Base
ndx
X
dist
⁡
ndx
D
=
Base
ndx
X
dist
⁡
ndx
D
3
2
1
tmslem
⊢
D
∈
∞Met
⁡
X
→
X
=
Base
K
∧
D
=
dist
⁡
K
∧
MetOpen
⁡
D
=
TopOpen
⁡
K
4
3
simp2d
⊢
D
∈
∞Met
⁡
X
→
D
=
dist
⁡
K