English
For anyOrderEmbedding f and HahnSeries x, the coefficient at f(a) of embDomain f x equals the coefficient at a of x.
Русский
Для любого отображения порядка f и Hahn-ряды x коэффициент при f(a) в embDomain f x равен коэффициенту при a в x.
LaTeX
$$$ (\\mathrm{embDomain} f\\,x).\\mathrm{coeff}(f a) = x.\\mathrm{coeff}(a) $$$
Lean4
@[simp]
theorem embDomain_coeff {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} : (embDomain f x).coeff (f a) = x.coeff a :=
by
rw [embDomain]
dsimp only
by_cases ha : a ∈ x.support
· rw [dif_pos (Set.mem_image_of_mem f ha)]
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)
· rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]
contrapose! ha
obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha
rwa [f.injective hb2] at hb1
