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]