ι : Sort ?u.84126
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
ι : Sort ?u.84126
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t u ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
rw [hausdorffEdist_comm] at fin
ι : Sort ?u.84126
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
ι : Sort ?u.84126
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
  hausdorffDist_triangle fin
no goals
ι : Sort ?u.84126
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
simpa [add_comm, hausdorffDist_comm] using I