English
Let R act on ℝ≥0 and on ENNReal with a scalar tower R → ℝ≥0 → ENNReal and ℝ≥0∞, and 0 is not a zero divisor. Then the natural embedding of NNReal into ENNReal respects the scalar action: ↑(r • s) = r • ↑s.
Русский
Пусть R действует на ℝ≥0 и ENNReal, образуя пирамиду скалярного действия R → ℝ≥0 → ENNReal, и 0 не делит ноль. Тогда естественное вложение NNReal в ENNReal совместимо с действием: ↑(r • s) = r • ↑s.
LaTeX
$$$\uparrow (r \cdot s) = r \cdot (\uparrow s).$$$
Lean4
theorem coe_smul {R} (r : R) (s : ℝ≥0) [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0] [IsScalarTower R ℝ≥0 ℝ≥0∞] :
(↑(r • s) : ℝ≥0∞) = (r : R) • (s : ℝ≥0∞) := by
rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc, one_mul]
