ι : Sort ?u.35077
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i s = 0
ι : Sort ?u.35077
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s s = 0
simp only [hausdorffEdist_def, sup_idem, ENNReal.iSup_eq_zero]
no goals
ι : Sort ?u.35077
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i s = 0
exact fun x hx => infEdist_zero_of_mem hx