instSMulPosReflectLE — Mathlib

English

If IsStrictOrderedModule holds for α and β, it holds for α and the dual β.

Русский

Если IsStrictOrderedModule справедливо для α и β, то справедливо и для α и двойственного β.

LaTeX

$$$[IsStrictOrderedModule α β] \\Rightarrow [IsStrictOrderedModule α β^{\\mathrm{op}}]$$$

Lean4

instance instSMulPosReflectLE [SMulPosReflectLE α β] : SMulPosReflectLE α βᵒᵈ where
  le_of_smul_le_smul_right _b hb a₁ a₂
    h := by
    rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg] at h
    exact le_of_smul_le_smul_right (β := β) h <| neg_pos.2 hb

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