exact hC x
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (1 + |x|) * ‖f x‖ ≤ C
no goals