English
Let m be a set-valued function on α with m(∅) = 0, and let c ≠ ∞ be a scalar in ENNReal. Then scaling the outer measure obtained from m by c gives exactly the outer measure obtained from the scaled function c • m (with the obvious zero on the empty set). In symbols, c • OuterMeasure.ofFunction(m, m_empty) = OuterMeasure.ofFunction(c • m, c • m_empty).
Русский
Пусть m — функция, сопоставляющая подмножества α значения в ENNReal, такая что m(∅) = 0, и пусть c ≠ ∞ — скаляр в ENNReal. Тогда умножение этой внешней меры на c равно внешней мере, построенной из функции c • m (с тем же нулём на пустом множестве). То есть c • OuterMeasure.ofFunction(m, m_empty) = OuterMeasure.ofFunction(c • m, c • m_empty).
LaTeX
$$$ c \\cdot \\mathrm{OuterMeasure.ofFunction}(m, m_{\\emptyset}) = \\mathrm{OuterMeasure.ofFunction}(c \\cdot m, c \\cdot m_{\\emptyset}) $$$
Lean4
theorem smul_ofFunction {c : ℝ≥0∞} (hc : c ≠ ∞) :
c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) (by simp [m_empty]) :=
by
ext1 s
haveI : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩
simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul, iInf_subtype']
rw [ENNReal.mul_iInf fun h => (hc h).elim]
