posMulReflectLT_iff_mulPosReflectLT

English

Let α be a commutative, zero-enabled ordered semigroup. Then the property PosMulReflectLT α holds if and only if MulPosReflectLT α holds.

Русский

Пусть α — коммутативное полугрупповое множество с нулём и упорядочением; тогда свойство PosMulReflectLT α эквивалентно свойству MulPosReflectLT α.

LaTeX

$$$PosMulReflectLT(\alpha) \iff MulPosReflectLT(\alpha)$$$

Lean4

theorem posMulReflectLT_iff_mulPosReflectLT : PosMulReflectLT α ↔ MulPosReflectLT α := by
  simp only [posMulReflectLT_iff, mulPosReflectLT_iff, Std.Commutative.comm]

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