English
For a finite set of indices, the sum inside setToFun equals the sum of individual setToFun evaluations, given integrability of each summand.
Русский
Для конечного числа индексов сумма функций внутри setToFun равна сумме отдельных значений при условии интегрируемости каждого слагаемого.
LaTeX
$$$\forall s: Finset ι, \forall (f : ι → α → E), (∀ i ∈ s, Integrable (f i) μ) \Rightarrow setToFun(μ, T) h_T (\sum i ∈ s, f i) = \sum i ∈ s, setToFun(μ, T) h_T (f i)$$$
Lean4
theorem setToFun_const [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) :
(setToFun μ T hT fun _ => x) = T univ x :=
by
have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm
rw [this]
exact setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x
