spectralValueTerms_finite_range — Mathlib

English

The range of spectralValueTerms(p) is a finite set for any polynomial p.

Русский

Область значений spectralValueTerms(p) является конечным множеством.

LaTeX

$$$$\operatorname{Set}.range\big(\operatorname{spectralValueTerms}(p)\big)\ \text{ is finite}. $$$$

Lean4

/-- The range of `spectralValue_terms p` is a finite set. -/
theorem spectralValueTerms_finite_range (p : R[X]) : (Set.range (spectralValueTerms p)).Finite :=
  Set.Finite.subset
      (Set.Finite.union (Set.finite_singleton 0) <|
        (Set.finite_Iio p.natDegree).image (fun n ↦ ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)))) <|
    by aesop (add simp [Set.range_subset_iff, spectralValueTerms])

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