continuous_descPochhammer_eval — Mathlib

English

The evaluation function x ↦ Polynomial.eval x (descPochhammer 𝕜 n) is continuous.

Русский

Функция x → Polynomial.eval x (descPochhammer 𝕜 n) непрерывна.

LaTeX

$$$$ \text{Continuous}\left( x \mapsto \mathrm{Polynomial.eval}(x, \mathrm{descPochhammer}(\mathbb{K}, n)) \right). $$$$

Lean4

/-- `descPochhammer 𝕜 n` is continuous. -/
theorem continuous_descPochhammer_eval : Continuous (descPochhammer 𝕜 n).eval := by
  exact differentiable_descPochhammer_eval.continuous

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