ι : Sort ?u.79415
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
ι : Sort ?u.79415
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
rw [hausdorffDist_comm] at H
ι : Sort ?u.79415
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist t s ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
ι : Sort ?u.79415
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
rw [hausdorffEdist_comm] at fin
no goals
ι : Sort ?u.79415
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist t s ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
simpa [dist_comm] using exists_dist_lt_of_hausdorffDist_lt h H fin