withZeroUnitsEquiv_symm_strictMono

English

Let α be a type with a linear ordered commutative group with zero. Then the inverse of the natural/unit equivalence coming from WithZero is strictly monotone.

Русский

Пусть α — множество с линейно упорядоченной коммутативной группой с нулем. Тогда обратное отображение естественного эквивалента единиц WithZero строго монотонно.

LaTeX

$$$\mathrm{StrictMono}\bigl((\mathrm{withZeroUnitsEquiv}(G := \alpha)).\mathrm{symm}\bigr)$$$

Lean4

theorem withZeroUnitsEquiv_symm_strictMono : StrictMono (withZeroUnitsEquiv (G := α)).symm :=
  OrderIso.withZeroUnits.symm.strictMono

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