F : Type ?u.302706
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} =
    sInf {x | ∃ h, { val := x, property := h } ∈ {C | ∀ (x : α), nndist (↑f x) (↑g x) ≤ C}}
F : Type ?u.302706
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (↑f x) (↑g x) ≤ C})
rw [val_eq_coe, coe_sInf, coe_image]
no goals
F : Type ?u.302706
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} =
    sInf {x | ∃ h, { val := x, property := h } ∈ {C | ∀ (x : α), nndist (↑f x) (↑g x) ≤ C}}
simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]