instSMulPosMono — Mathlib

English

If each component β_i has PosSMulMono, then the lifted structure on the Pi-type β ≔ (i ↦ β_i) yields a PosSMulMono; scalar action is defined componentwise and preserves order componentwise.

Русский

Если каждый компонент β_i удовлетворяет PosSMulMono, то поднятая структура на Π-типе β ≔ (i ↦ β_i) задаёт PosSMulMono; скалярное действие определяется по компонентам и сохраняет порядок по компонентам.

LaTeX

$$$\mathrm{PosSMulMono}\;\alpha\;((i \mapsto \beta_i))$$$

Lean4

instance instSMulPosMono [∀ i, SMulPosMono α (β i)] : SMulPosMono α (∀ i, β i) where
  smul_le_smul_of_nonneg_right _b hb _a₁ _a₂ ha i := smul_le_smul_of_nonneg_right ha (hb i)

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