embDomain_zero — Mathlib

English

Let f be an order-embedding from Γ to Γ'. Then applying the embedding to the zero Hahn series yields the zero Hahn series: embDomain f (0) = 0.

Русский

Пусть f : Γ ↪o Γ' — отображение с полем порядка. Тогда отображение embDomain f нулевой Hahn-ряд переходит в нулевой Hahn-ряд: embDomain f (0) = 0.

LaTeX

$$$ embDomain\;f\;0 = 0 $$$

Lean4

@[simp]
theorem embDomain_zero {f : Γ ↪o Γ'} : embDomain f (0 : HahnSeries Γ R) = 0 :=
  by
  ext
  simp [embDomain_notin_image_support]

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