instPosSMulReflectLT — Mathlib

English

The dual order supports PosSMulReflectLE provided the base supports it; the LE-structure lifts to the dual.

Русский

Двойственный порядок поддерживает PosSMulReflectLE, если базовый порядок поддерживает это; структура LE поднимается к двойственному порядку.

LaTeX

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

Lean4

instance instPosSMulReflectLT [PosSMulReflectLT α β] : PosSMulReflectLT α βᵒᵈ where
  lt_of_smul_lt_smul_left _a ha _b₁ _b₂ h := lt_of_smul_lt_smul_of_nonneg_left (β := β) h ha

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