exists_forall_norm_le — Mathlib

English

In a proper space, for any polynomial p ∈ R[X] there exists x ∈ R such that ∥p(x)∥ ≤ ∥p(y)∥ for all y ∈ R.

Русский

В корректном пространстве для любого p ∈ R[X] существует x ∈ R, такое что ∥p(x)∥ ≤ ∥p(y)∥ для всех y ∈ R.

LaTeX

$$$\\exists x \\in R, \\; \\forall y \\in R,\\; \\|p(x)\\| \\le \\|p(y)\\|$$$

Lean4

theorem exists_forall_norm_le [ProperSpace R] (p : R[X]) : ∃ x, ∀ y, ‖p.eval x‖ ≤ ‖p.eval y‖ :=
  if hp0 : 0 < degree p then p.continuous.norm.exists_forall_le <| p.tendsto_norm_atTop hp0 tendsto_norm_cocompact_atTop
  else ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩

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