Database
BASIC TOPOLOGY
Metric spaces
Open sets of a metric space
mstopn
Metamath Proof Explorer
Description: The topology component of a metric space coincides with the topology
generated by the metric component. (Contributed by Mario Carneiro , 26-Aug-2015)
Ref
Expression
Hypotheses
isms.j
⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
isms.x
⊢ 𝑋 = ( Base ‘ 𝐾 )
isms.d
⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion
mstopn
⊢ ( 𝐾 ∈ MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )
Proof
Step
Hyp
Ref
Expression
1
isms.j
⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
2
isms.x
⊢ 𝑋 = ( Base ‘ 𝐾 )
3
isms.d
⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
4
1 2 3
isms2
⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
5
4
simprbi
⊢ ( 𝐾 ∈ MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )