ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ((⨆ (x : α) (_ : x ∈ s), infEdist x u) ⊔ ⨆ (y : α) (_ : y ∈ u), infEdist y s) ≤
    hausdorffEdist s t + hausdorffEdist t u
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u
rw [hausdorffEdist_def]
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ (∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧
    ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ((⨆ (x : α) (_ : x ∈ s), infEdist x u) ⊔ ⨆ (y : α) (_ : y ∈ u), infEdist y s) ≤
    hausdorffEdist s t + hausdorffEdist t u
simp only [sup_le_iff, iSup_le_iff]
case left
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u

case right
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ (∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧
    ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
constructor
case left
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ s → infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
case left
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u
show ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
no goals
case left
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ s → infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
exact fun x xs =>
  calc
    infEdist x u ≤ infEdist x t + hausdorffEdist t u :=
      infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist s t + hausdorffEdist t u :=
      add_le_add_right (infEdist_le_hausdorffEdist_of_mem xs) _
case right
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ u → infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
case right
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
show ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
no goals
case right
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ u → infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
exact fun x xu =>
  calc
    infEdist x s ≤ infEdist x t + hausdorffEdist t s :=
      infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist u t + hausdorffEdist t s :=
      add_le_add_right (infEdist_le_hausdorffEdist_of_mem xu) _
    _ = hausdorffEdist s t + hausdorffEdist t u := by simp [hausdorffEdist_comm, add_comm]
no goals
ι : Sort ?u.46441
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
x : α
xu : x ∈ u
⊢ hausdorffEdist u t + hausdorffEdist t s = hausdorffEdist s t + hausdorffEdist t u
simp [hausdorffEdist_comm, add_comm]