English
If each component β_i has the PosSMulMono property, then the Pi-type ∀ i, β_i also has a pointwise monotone scalar action: for any a ≥ 0 and f ≤ g (pointwise), a • f ≤ a • g (pointwise).
Русский
Если каждый компонент β_i обладает свойством PosSMulMono, то Π-тип ∀ i, β_i также имеет покомпонентную монотонность скалярного умножения: для любого а ≥ 0 выполняется a • f ≤ a • g по каждой компоненте, если f ≤ g покомпонентно.
LaTeX
$$$\forall a \ge 0,\ \forall f,g:\prod_{i} \beta_i,\ f \le g \Rightarrow a \cdot f \le a \cdot g,$$$
Lean4
instance instPosSMulMono [∀ i, PosSMulMono α (β i)] : PosSMulMono α (∀ i, β i) where
smul_le_smul_of_nonneg_left _a ha _b₁ _b₂ hb i := smul_le_smul_of_nonneg_left (hb i) ha
