le_gaussNorm — Mathlib

English

If the set {v(f_i) c^i} is bounded above, then for each i we have v(f_i) c^i ≤ gaussNorm(v,c,f).

Русский

Если множество значений {v(f_i) c^i} ограничено сверху, то для любого i выполняется неравенство v(f_i) c^i ≤ gaussNorm(v,c,f).

LaTeX

$$$ BddAbove\ (\{ x \mid \exists i, v(f_{i}) c^{i} = x\}) \Rightarrow \forall i,\; v(f_{i}) c^{i} \le \mathrm{gaussNorm}(v,c,f) $$$

Lean4

theorem le_gaussNorm (hbd : BddAbove {x | ∃ i, v (f.coeff i) * c ^ i = x}) (i : ℕ) :
    v (f.coeff i) * c ^ i ≤ f.gaussNorm v c :=
  le_ciSup hbd i

Похожие утверждения