English
The span of a finite set s of polynomials is contained in degreeLE(R,n) for some n.
Русский
Образование(span) конечного набора многочленов содержится в degreeLE(R,n) для некоторого n.
LaTeX
$$$\exists n \; Submodule.span_R s \le \operatorname{degreeLE}_R(n).$$$
Lean4
/-- The span of every finite set of polynomials is contained in a `degreeLE n` for some `n`. -/
theorem span_le_degreeLE_of_finite {s : Set R[X]} (s_fin : s.Finite) : ∃ n : ℕ, Submodule.span R s ≤ degreeLE R n :=
by
by_cases s_emp : s.Nonempty
· rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩
exact ⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩
· rw [Set.not_nonempty_iff_eq_empty] at s_emp
rw [s_emp, Submodule.span_empty]
exact ⟨0, bot_le⟩
