PosSMulReflectLE_iff_posSMulReflectLT

English

PosSMulReflectLE and PosSMulReflectLT are interchangeable; one can derive LE-reflection from LT-reflection and vice versa.

Русский

Обратимость отражений LE и LT для PosSMul: можно перейти от LT к LE и обратно.

LaTeX

$$$\\text{PosSMulReflectLE } α β \\iff \\text{PosSMulReflectLT } α β$$$

Lean4

theorem PosSMulReflectLE_iff_posSMulReflectLT : PosSMulReflectLE α β ↔ PosSMulReflectLT α β :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ PosSMulReflectLT.toPosSMulReflectLE⟩

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