α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ ∀ (x y : α × Closeds α), infEdist x.fst ↑x.snd ≤ infEdist y.fst ↑y.snd + 2 * edist x y
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ Continuous fun p => infEdist p.fst ↑p.snd
refine' continuous_of_le_add_edist 2 (by simp) _
case mk.mk
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist (x, s).fst ↑(x, s).snd ≤ infEdist (y, t).fst ↑(y, t).snd + 2 * edist (x, s) (y, t)
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ ∀ (x y : α × Closeds α), infEdist x.fst ↑x.snd ≤ infEdist y.fst ↑y.snd + 2 * edist x y
rintro ⟨x, s⟩ ⟨y, t⟩
no goals
case mk.mk
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist (x, s).fst ↑(x, s).snd ≤ infEdist (y, t).fst ↑(y, t).snd + 2 * edist (x, s) (y, t)
calc
  infEdist x s ≤ infEdist x t + hausdorffEdist (t : Set α) s :=
    infEdist_le_infEdist_add_hausdorffEdist
  _ ≤ infEdist y t + edist x y + hausdorffEdist (t : Set α) s :=
    (add_le_add_right infEdist_le_infEdist_add_edist _)
  _ = infEdist y t + (edist x y + hausdorffEdist (s : Set α) t) := by
    rw [add_assoc, hausdorffEdist_comm]
  _ ≤ infEdist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) :=
    (add_le_add_left (add_le_add (le_max_left _ _) (le_max_right _ _)) _)
  _ = infEdist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]
no goals
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ 2 ≠ ⊤
simp
no goals
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + edist x y + hausdorffEdist ↑t ↑s = infEdist y ↑t + (edist x y + hausdorffEdist ↑s ↑t)
rw [add_assoc, hausdorffEdist_comm]
no goals
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t)) = infEdist y ↑t + 2 * edist (x, s) (y, t)
rw [← mul_two, mul_comm]