English
The value of evalCoeff is independent of the choice of y when hy is fixed.
Русский
Значение evalCoeff не зависит от выбора y при фиксированном hy.
LaTeX
$$$ f.evalCoeff x c = (ofLex (f.val y)).coeff c $$$
Lean4
/-- The coefficient is well-defined regardless of which `y` we pick in `evalCoeff`. -/
theorem evalCoeff_eq [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : f.val.domain}
(hy : y.val - x ∈ ball K c) : evalCoeff f x c = (ofLex (f.val y)).coeff c :=
by
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K c := ⟨y, hy⟩
simpa [evalCoeff, hnonempty] using coeff_eq_of_mem f x hnonempty.choose_spec hy (le_refl _)