ι : Sort ?u.83408
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
ι : Sort ?u.83408
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
refine toReal_le_add' hausdorffEdist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
ι : Sort ?u.83408
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
ι : Sort ?u.83408
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
rw [hausdorffEdist_comm] at fin
no goals
ι : Sort ?u.83408
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEdist_triangle