instSMulPosMono — Mathlib

English

If SMulPosStrictMono holds for α and β, it also holds for the OrderDual β.

Русский

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

LaTeX

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

Lean4

instance instSMulPosMono [SMulPosMono α β] : SMulPosMono α βᵒᵈ where
  smul_le_smul_of_nonneg_right _b hb a₁ a₂
    ha := by
    rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
    exact smul_le_smul_of_nonneg_right (β := β) ha <| neg_nonneg.2 hb

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