instPosSMulReflectLE — Mathlib

English

The dual order inherits a PosSMulReflectLE structure from the base PosSMulReflectLE.

Русский

Двойственный порядок наследует структуру PosSMulReflectLE от базового.

LaTeX

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

Lean4

instance instPosSMulReflectLE [PosSMulReflectLE α β] : PosSMulReflectLE α βᵒᵈ where
  le_of_smul_le_smul_left _a ha _b₁ _b₂ h := le_of_smul_le_smul_of_pos_left (β := β) h ha

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