orderedSMul — Mathlib

English

If each component M_i carries an OrderedSMul by 𝕜, then the function space ∀ i, M_i carries an OrderedSMul by 𝕜 with pointwise action.

Русский

Если каждый компонент M_i имеет OrderedSMul 𝕜, то пространство функций ∀ i, M_i имеет упорядоченное умножение 𝕜 с покомпонентным действием.

LaTeX

$$$ OrderedSMul\ 𝕜\ (\{M_i\}_{i}) $$$

Lean4

instance orderedSMul {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, PartialOrder (M i)]
    [∀ i, MulActionWithZero 𝕜 (M i)] [∀ i, OrderedSMul 𝕜 (M i)] : OrderedSMul 𝕜 (∀ i, M i) :=
  OrderedSMul.mk' fun _ _ _ h hc i => smul_le_smul_of_nonneg_left (h.le i) hc.le

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