toOrderAddMonoidHom_injective — Mathlib

English

The map f.toOrderAddMonoidHom is injective; different partial embeddings have distinct order-preserving representations.

Русский

Отображение f.toOrderAddMonoidHom инъективно; разные частичные вложения порождают разные представления.

LaTeX

$$$\text{Injective}(f.toOrderAddMonoidHom)$$$

Lean4

theorem toOrderAddMonoidHom_injective : Function.Injective f.toOrderAddMonoidHom :=
  f.prop.strictMono.injective

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