posSMulMono_iff_posSMulStrictMono

English

Under appropriate order and module structures, PosSMulMono is equivalent to PosSMulStrictMono.

Русский

При надлежащих условиях порядка и модуля монотонность слева эквивалентна строгой монотонности слева.

LaTeX

$$$\\text{PosSMulMono } α β \\quad\\Leftrightarrow\\quad \\text{PosSMulStrictMono } α β$$$

Lean4

theorem posSMulMono_iff_posSMulStrictMono : PosSMulMono α β ↔ PosSMulStrictMono α β :=
  ⟨fun _ ↦ PosSMulMono.toPosSMulStrictMono, fun _ ↦ inferInstance⟩

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