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]