evalCoeff_eq — Mathlib

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 _)

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