no goals
ι : Sort ?u.53920
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure t) = hausdorffEdist s t
simp [@hausdorffEdist_comm _ _ s _]