smul_iSup — Mathlib

English

Let R be a scalar type with SMul on ENNReal and an IsScalarTower condition. For any f : ι → OuterMeasure α and c ∈ R, the scalar action distributes over iSup: c • (⨆ i, f i) = ⨆ i, c • f i.

Русский

Пусть R — множество скаляров с операцией умножения над ENNReal и соблюдается условие IsScalarTower. Для любой f : ι → OuterMeasure α и скаляра c ∈ R выполняется: c • (⨆ i, f i) = ⨆ i, c • f i.

LaTeX

$$$ (c \cdot (\big\vee_{i} f_i)) = \big\vee_{i} (c \cdot f_i) $$$

Lean4

theorem smul_iSup {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {ι : Sort*} (f : ι → OuterMeasure α) (c : R) :
    (c • ⨆ i, f i) = ⨆ i, c • f i :=
  ext fun s => by simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]

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