English
The relation f.toOrderAddMonoidHom x = f.val x holds for all x in the domain.
Русский
Всем x из области определения выполняется: f.toOrderAddMonoidHom x = f.val x.
LaTeX
$$$ f.toOrderAddMonoidHom\ x = f.val\ x $$$
Lean4
theorem apply_of_mem_stratum {x : f.val.domain} {c : FiniteArchimedeanClass M} (hx : x.val ∈ seed.stratum c.val) :
f.val x = toLex (HahnSeries.single c (seed.coeff c.val ⟨x.val, hx⟩)) :=
by
have hx' : x.val ∈ seed.baseEmbedding.domain := seed.mem_domain_baseEmbedding hx
have heq : (⟨x.val, hx'⟩ : seed.baseEmbedding.domain).val = x.val := rfl
rw [← f.prop.baseEmbedding_le.2 heq]
let fx : Π₀ c, seed.stratum c := DFinsupp.single c ⟨x.val, hx⟩
have hfx : x.val = fx.sum fun c ↦ (seed.stratum c).subtype := by simp [fx, DFinsupp.sum_single_index]
apply_fun ofLex
rw [ofLex_toLex]
ext d
rw [seed.coeff_baseEmbedding hfx]
unfold fx
obtain rfl | hdc := eq_or_ne d c
· simp
have hcd : c.val ≠ d.val := Subtype.ext_iff.ne.mp hdc.symm
simp [HahnSeries.coeff_single_of_ne hdc, hcd]
