instSMulPosReflectLT — Mathlib

English

The dual order supports IsOrderedModule when IsOrderedModule is given.

Русский

Двойственный порядок поддерживает IsOrderedModule, когда дано IsOrderedModule.

LaTeX

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

Lean4

instance instSMulPosReflectLT [SMulPosReflectLT α β] : SMulPosReflectLT α βᵒᵈ where
  lt_of_smul_lt_smul_right _b hb a₁ a₂
    h := by
    rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg] at h
    exact lt_of_smul_lt_smul_right (β := β) h <| neg_nonneg.2 hb

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