embDomain_mk_coeff — Mathlib

English

If f is built as an order-embedding from a function with a left inverse property, then the same coefficient preservation holds for embDomain using the constructed embedding.

Русский

Если f-создано как отображение порядка с обратной связью по левой стороне, то сохранение коэффициента сохраняется и для embDomain, использующего полученное вложение.

LaTeX

$$$ (\\mathrm{embDomain}(\\langle \\langle f, hfi \\rangle, hf \\rangle) x).\\mathrm{coeff}(f a) = x.\\mathrm{coeff}(a) $$$

Lean4

@[simp]
theorem embDomain_mk_coeff {f : Γ → Γ'} (hfi : Function.Injective f) (hf : ∀ g g' : Γ, f g ≤ f g' ↔ g ≤ g')
    {x : HahnSeries Γ R} {a : Γ} : (embDomain ⟨⟨f, hfi⟩, hf _ _⟩ x).coeff (f a) = x.coeff a :=
  embDomain_coeff

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