English
The support of evalCoeff is well-founded (no infinite descending chain).
Русский
Опора evalCoeff ограничена и не содержит бесконечных нисходящих цепочек.
LaTeX
$$$ (f.evalCoeff x).support.IsWF $$$
Lean4
theorem isWF_support_evalCoeff [IsOrderedAddMonoid R] [Archimedean R] (x : M) : (evalCoeff f x).support.IsWF :=
by
rw [Set.isWF_iff_no_descending_seq]
by_contra!
obtain ⟨seq, ⟨hanti, hmem⟩⟩ := this
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K (seq 0) :=
by
specialize hmem 0
contrapose hmem with hempty
simp [evalCoeff, hempty]
obtain ⟨y, hy⟩ := hnonempty
have hmem' (n : ℕ) : seq n ∈ (ofLex (f.val y)).coeff.support :=
by
specialize hmem n
rw [Function.mem_support] at ⊢ hmem
convert hmem using 1
refine (f.evalCoeff_eq (ball_antitone K ?_ hy)).symm
simpa using hanti.antitone (show 0 ≤ n by simp)
obtain hwf := (ofLex (f.val y)).isWF_support
contrapose! hwf
rw [Set.isWF_iff_no_descending_seq]
simpa using ⟨seq, hanti, hmem'⟩
