spectralValueTerms_bddAbove — Mathlib

English

The set of spectralValueTerms(p)(n) for n ∈ ℕ is bounded above.

Русский

Набор значений spectralValueTerms(p)(n) по n ограничен сверху.

LaTeX

$$$$\exists M\in\mathbb{R}_{+}\;\forall n\in\mathbb{N},\ \operatorname{spectralValueTerms}(p)(n)\le M.$$$$

Lean4

/-- The sequence `spectralValue_terms p` is bounded above. -/
theorem spectralValueTerms_bddAbove (p : R[X]) : BddAbove (Set.range (spectralValueTerms p)) :=
  (spectralValueTerms_finite_range p).bddAbove

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