toSMulPosReflectLE — Mathlib

English

If SMulPosStrictMono holds, then SMulPosReflectLE holds: left-multiplication by nonnegative scalars preserves and reflects order in the ≤ sense.

Русский

Если SMulPosStrictMono выполняется, тогда SMulPosReflectLE выполняется: умножение слева на неотрицательные скаляры сохраняет и отражает порядок по отношению к нестрогому ≤.

LaTeX

$$SMulPosStrictMono\\,\\alpha\\,\\beta \\Rightarrow SMulPosReflectLE\\,\\alpha\\,\\beta$$

Lean4

instance (priority := 100) toSMulPosReflectLE [SMulPosStrictMono α β] : SMulPosReflectLE α β where
  le_of_smul_le_smul_right _b hb _a₁ _a₂ h := not_lt.1 fun ha ↦ h.not_gt <| smul_lt_smul_of_pos_right ha hb

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