mulPosReflectLE_iff_mulPosReflectLT

English

For a cancellative monoid with zero with a partial order, the property MulPosReflectLE is equivalent to MulPosReflectLT: having left multiplication that preserves or reflects LE is equivalent to having it reflect LT.

Русский

Для отменяемого моноида с нулём с частичным порядком свойство MulPosReflectLE эквивалентно MulPosReflectLT: сохранение или отражение LE эквивалентно отражению LT левой умножением.

LaTeX

$$$\text{MulPosReflectLE}(\alpha) \iff \text{MulPosReflectLT}(\alpha)$$

Lean4

theorem mulPosReflectLE_iff_mulPosReflectLT : MulPosReflectLE α ↔ MulPosReflectLT α :=
  ⟨@MulPosReflectLE.toMulPosReflectLT α _ _, @MulPosReflectLT.toMulPosReflectLE α _ _⟩

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