toOrderAddMonoidHom_apply — Mathlib

English

The evaluation map for a partial Hahn embedding applied to x agrees with the underlying linear map: f.toOrderAddMonoidHom x = f.val x.

Русский

Отображение `toOrderAddMonoidHom` на x совпадает с исходным линейным отображением: f.toOrderAddMonoidHom x = f.val x.

LaTeX

$$$ f.toOrderAddMonoidHom\ x = f.val\ x $$$

Lean4

theorem toOrderAddMonoidHom_apply (x : f.val.domain) : f.toOrderAddMonoidHom x = f.val x :=
  rfl

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