English
Let x ∈ seed.baseEmbedding.domain and f a finitely supported function over strata with x = sum_c f(c)·(stratum c). Then the coefficient of ofLex (baseEmbedding seed x) at c equals seed.coeff c (f(c)).
Русский
Пусть x ∈ области базового вложения и f имеет конечную опору по слоям так, что x = ∑_c f(c)·(слой c). Тогда коэффициент у ofLex (baseEmbedding seed x) в позиции c равен seed.coeff c (f(c)).
LaTeX
$$$\text{For } x: seed.baseEmbedding \text{ domain},\ f: \Pi_0 c,\ seed.stratum c,\ (h): x = \sum c \mapsto (seed.stratum c).subtype\, ,\ (c) : \ (ofLex( baseEmbedding(seed) x)).coeff\, c = seed.coeff\, c\, (f\, c) $$$
Lean4
theorem coeff_baseEmbedding {x : seed.baseEmbedding.domain} {f : Π₀ c, seed.stratum c}
(h : x.val = f.sum fun c ↦ (seed.stratum c).subtype) (c : FiniteArchimedeanClass M) :
(ofLex ((baseEmbedding seed) x)).coeff c = seed.coeff c (f c) := by
simpa [baseEmbedding] using seed.hahnCoeff_apply h c.val
