Database
BASIC TOPOLOGY
Metric spaces
Metric space balls
blrnps
Metamath Proof Explorer
Description: Membership in the range of the ball function. Note that
ran ( ball D ) is the collection of all balls for metric D .
(Contributed by NM , 31-Aug-2006) (Revised by Mario Carneiro , 12-Nov-2013) (Revised by Thierry Arnoux , 11-Mar-2018)
Ref
Expression
Assertion
blrnps
⊢ D ∈ PsMet ⁡ X → A ∈ ran ⁡ ball ⁡ D ↔ ∃ x ∈ X ∃ r ∈ ℝ * A = x ball ⁡ D r
Proof
Step
Hyp
Ref
Expression
1
blfps
⊢ D ∈ PsMet ⁡ X → ball ⁡ D : X × ℝ * ⟶ 𝒫 X
2
ffn
⊢ ball ⁡ D : X × ℝ * ⟶ 𝒫 X → ball ⁡ D Fn X × ℝ *
3
ovelrn
⊢ ball ⁡ D Fn X × ℝ * → A ∈ ran ⁡ ball ⁡ D ↔ ∃ x ∈ X ∃ r ∈ ℝ * A = x ball ⁡ D r
4
1 2 3
3syl
⊢ D ∈ PsMet ⁡ X → A ∈ ran ⁡ ball ⁡ D ↔ ∃ x ∈ X ∃ r ∈ ℝ * A = x ball ⁡ D r