Theorem: bound_forall (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
ι : Type u_3
s : Finset ι
f : ι → E → ℝ
h : ∀ i ∈ s, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i ∈ s, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
sorry
State after:
no goals