English
If y and z are both near x within ball K c, then the initial coefficients of f.val y and f.val z agree for all d ≤ c.
Русский
Если y и z близки к x внутри шара K c, то начальные коэффициенты f.val y и f.val z совпадают для всех d ≤ c.
LaTeX
$$$$ (ofLex (f.val y)).coeff d = (ofLex (f.val z)).coeff d \quad\text{for all } d \le c $$$$
Lean4
/-- When `y` and `z` are both near `x` (the difference is in a ball),
initial coefficients of `f.val y` and `f.val z` agree. -/
theorem coeff_eq_of_mem [IsOrderedAddMonoid R] [Archimedean R] (x : M) {y z : f.val.domain} {c : ArchimedeanClass M}
(hy : y.val - x ∈ ball K c) (hz : z.val - x ∈ ball K c) {d : FiniteArchimedeanClass M} (hd : d ≤ c) :
(ofLex (f.val y)).coeff d = (ofLex (f.val z)).coeff d :=
by
apply eq_of_sub_eq_zero
rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub]
refine coeff_eq_zero_of_mem f ?_ hd
have : (y - z).val = (y.val - x) - (z.val - x) := by
push_cast
simp
rw [this]
exact Submodule.sub_mem _ hy hz
