exists_min_root — Mathlib

English

Let R be a domain with a LinearOrder. If p ∈ R[X] and p ≠ 0, then there exists x0 ∈ R such that for every root x of p we have x0 ≤ x.

Русский

Пусть R обладает линейным порядком. Если p ∈ R[X] и p ≠ 0, то существует x0 ∈ R такой, что для каждого корня x выполняется x0 ≤ x.

LaTeX

$$$ [LinearOrder\ R] \ p : R[X],\ p \neq 0 \Rightarrow \exists x_0 \in R, \forall x \in R, p.IsRoot x \Rightarrow x_0 \le x $$$

Lean4

theorem exists_min_root [LinearOrder R] (p : R[X]) (hp : p ≠ 0) : ∃ x₀, ∀ x, p.IsRoot x → x₀ ≤ x :=
  Set.exists_lower_bound_image _ _ <| finite_setOf_isRoot hp

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