instPosSMulReflectLE — Mathlib

English

If every component β_i has PosSMulMono, then the Pi-type ∀ i, β_i satisfies PosSMulMono with pointwise order and componentwise scalar action.

Русский

Если каждый компонент β_i обладает PosSMulMono, то Π-тип ∀ i, β_i удовлетворяет PosSMulMono с точечно заданным порядком и по-компонентному скалярному действию.

LaTeX

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

Lean4

instance instPosSMulReflectLE [∀ i, PosSMulReflectLE α (β i)] : PosSMulReflectLE α (∀ i, β i) where
  le_of_smul_le_smul_left _a ha _b₁ _b₂ h i := le_of_smul_le_smul_left (h i) ha

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