toPosSMulReflectLE — Mathlib

English

If a left action has PosSMulMono and PosSMulLT-reflection properties, then any LE-reflection instance yields LT-reflection and vice versa.

Русский

Если левое действие имеет положительную монотонность и отражение LE/LT, то отражение LE эквивалентно отражению LT и наоборот.

LaTeX

$$$\\text{PosSMulMono } α β \\;\\text{and}\\; \\text{PosSMulLT reflection} \\Rightarrow (PosSMulLE \\iff PosSMulLT)$$$

Lean4

instance toPosSMulReflectLE [PosSMulReflectLT α β] : PosSMulReflectLE α β :=
  ⟨fun _a ha _b₁ _b₂ h ↦
    h.eq_or_lt.elim (fun h ↦ (smul_right_injective _ ha.ne' h).le) fun h' ↦ (lt_of_smul_lt_smul_left h' ha.le).le⟩

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