toOrderIso_injective — Mathlib

English

The map that sends an ordered monoid isomorphism to its associated order isomorphism is injective.

Русский

Отображение, переводящее упорядоченный моноидный изоморфизм в соответствующий изоморфизм порядка, инъективно.

LaTeX

$$$Injective\left(toOrderIso : _ \to α \simeq_o β\right).$$$

Lean4

@[to_additive]
theorem toOrderIso_injective : Injective (toOrderIso : _ → α ≃o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

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