English
If c ≠ 0, scaling commutes with extension: c • extend m = extend (s ↦ c • m s).
Русский
Если скаляр c не равен нулю, умножение на c и расширение коммутируют: c • extend m = extend (s ↦ c • m s).
LaTeX
$$$c \\neq 0 \\Rightarrow c \\cdot \\mathrm{extend}\, m = \\mathrm{extend}\\, (\\lambda s\\, h \\to c \\cdot m\\, s\\; h)$$$
Lean4
theorem smul_extend {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [NoZeroSMulDivisors R ℝ≥0∞] {c : R}
(hc : c ≠ 0) : c • extend m = extend fun s h => c • m s h := by
classical
ext1 s
dsimp [extend]
by_cases h : P s
· simp [h]
· simp [h, ENNReal.smul_top, hc]