smul_extend — Mathlib

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]

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