exists C + ‖y‖
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∀ (x : ℝ), ‖φ x - y‖ ≤ C + ‖y‖