smul_iSup — Mathlib

English

General distributivity of scalar multiplication over iSup in ENNReal under a tensor/tower structure.

Русский

Обобщённая формула распределения скалярного умножения над iSup в ENNReal с использованием структуры тензора/степени.

LaTeX

$$$c \\cdot \\left( \\bigvee_i f_i \\right) = \\bigvee_i c \\cdot f_i$$$

Lean4

theorem smul_iSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (f : ι → ℝ≥0∞) (c : R) : c • ⨆ i, f i = ⨆ i, c • f i :=
  by simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

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