ι : Sort ?u.56722
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ (⨅ (i : { y // y ∈ s }), ENNReal.toReal (edist x ↑i)) = ⨅ (y : ↑s), dist x ↑y

ι : Sort ?u.56722
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ∀ (i : { y // y ∈ s }), edist x ↑i ≠ ⊤
ι : Sort ?u.56722
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x s = ⨅ (y : ↑s), dist x ↑y
rw [infDist, infEdist, iInf_subtype', ENNReal.toReal_iInf]
no goals
ι : Sort ?u.56722
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ (⨅ (i : { y // y ∈ s }), ENNReal.toReal (edist x ↑i)) = ⨅ (y : ↑s), dist x ↑y
simp only [dist_edist]
no goals
ι : Sort ?u.56722
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ∀ (i : { y // y ∈ s }), edist x ↑i ≠ ⊤
exact fun _ ↦ edist_ne_top _ _