toSMulPosReflectLE — Mathlib

English

Equivalences between LE and LT reflections propagate through the SMul structure.

Русский

Эквивалентности между отражениями LE и LT распространяются через скалярное умножение.

LaTeX

$$$[PosSMulReflectLE α β] \\iff [PosSMulReflectLT α β]$$$

Lean4

theorem toSMulPosReflectLE [SMulPosReflectLT α β] : SMulPosReflectLE α β :=
  ⟨fun _b hb _a₁ _a₂ h ↦
    h.eq_or_lt.elim (fun h ↦ (smul_left_injective _ hb.ne' h).le) fun h' ↦ (lt_of_smul_lt_smul_right h' hb.le).le⟩

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