embDomain_injective — Mathlib

English

For any order-embedding f, the map embDomain f is injective.

Русский

Для любого вложения типа OrderEmbedding f отображение embDomain f является инъективным.

LaTeX

$$embDomain f is injective$$

Lean4

theorem embDomain_injective {f : Γ ↪o Γ'} : Function.Injective (embDomain f : HahnSeries Γ R → HahnSeries Γ' R) :=
  fun x y xy => by
  ext g
  rw [HahnSeries.ext_iff, funext_iff] at xy
  have xyg := xy (f g)
  rwa [embDomain_coeff, embDomain_coeff] at xyg

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