Theorem: CS.bounded (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x v : ℝ
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
Tactic:
obtain ⟨x, hx⟩ := (continuous_norm.comp f.continuous).exists_forall_ge_of_hasCompactSupport f.h2.norm
State after:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x✝ v x : ℝ
hx : ∀ (y : ℝ), ((fun a => ‖a‖) ∘ f.toFun) y ≤ ((fun a => ‖a‖) ∘ f.toFun) x
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C

State before:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x✝ v x : ℝ
hx : ∀ (y : ℝ), ((fun a => ‖a‖) ∘ f.toFun) y ≤ ((fun a => ‖a‖) ∘ f.toFun) x
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
Tactic:
exact ⟨_, hx⟩
State after:
no goals