English
Let α be a nonempty set and E, F, F' be normed spaces. For any rule T that assigns to each subset S ⊆ α a continuous linear map T(S): F → F', and for any x ∈ F, the simple function obtained by taking the constant value x on every point of α equals the global action of T on the whole domain applied to x; i.e., the simple function built from the constant x is T(univ) applied to x.
Русский
Пусть α непустое множество, а E, F, F' — нормированные пространства. Для любой правила T, которое каждому подмножеству S ⊆ α ставит непрерывно-линейное отображение T(S): F → F', и для любого x ∈ F, простая функция, задаваемая константное значение x на всей α, равна действию T на все α, применённому к x; то есть простая функция, константная на α, равна T(омегу) x.
LaTeX
$$$ \mathrm{setToSimpleFunc}(T, \mathrm{const}_{\alpha}(x)) = T(\mathrm{univ})\,x $$$
Lean4
theorem setToSimpleFunc_const' [Nonempty α] (T : Set α → F →L[ℝ] F') (x : F) {m : MeasurableSpace α} :
SimpleFunc.setToSimpleFunc T (SimpleFunc.const α x) = T univ x := by
simp only [setToSimpleFunc, range_const, Set.mem_singleton, preimage_const_of_mem, sum_singleton,
← Function.const_def, coe_const]
