English
If s is a finite set of polynomials and p lies in the span of s, then there exists p' ∈ s with deg p ≤ deg p'.
Русский
Если s—конечный набор многочленов, и p лежит в образовании span(s), то существует p' ∈ s с deg p ≤ deg p'.
LaTeX
$$$\exists p' \in s, \deg p \le \deg p'.$$$
Lean4
/-- A stronger version of `Polynomial.exists_degree_le_of_mem_span` under the assumption that the
set `s : R[X]` is finite. There exists a polynomial `p' ∈ s` whose degree dominates the degree of
every element of `p ∈ span R s`. -/
theorem exists_degree_le_of_mem_span_of_finite {s : Set R[X]} (s_fin : s.Finite) (hs : s.Nonempty) :
∃ p' ∈ s, ∀ (p : R[X]), p ∈ Submodule.span R s → degree p ≤ degree p' :=
by
obtain ⟨a, has, hmax⟩ := s_fin.exists_maximalFor degree s hs
refine ⟨a, has, fun p hp => ?_⟩
obtain ⟨p', hp', hpp'⟩ := exists_degree_le_of_mem_span hs hp
exact hpp'.trans <| not_lt.1 <| not_lt_iff_le_imp_ge.2 <| hmax hp'
