setToSimpleFunc_const — Mathlib

English

Let α be any set (not necessarily nonempty). For any T as above and x ∈ F, the same equality holds: the simple function formed by the constant x on α is T(univ) x.

Русский

Пусть α — произвольное множество. Для любого T и x ∈ F верно равенство: простая функция, константная на α, равна T(univ) x.

LaTeX

$$$ \mathrm{setToSimpleFunc}(T, \mathrm{const}_{\alpha}(x)) = T(\mathrm{univ})\,x $$$

Lean4

theorem setToSimpleFunc_const (T : Set α → F →L[ℝ] F') (hT_empty : T ∅ = 0) (x : F) {m : MeasurableSpace α} :
    SimpleFunc.setToSimpleFunc T (SimpleFunc.const α x) = T univ x :=
  by
  cases isEmpty_or_nonempty α
  · have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
    rw [h_univ_empty, hT_empty]
    simp only [setToSimpleFunc, ContinuousLinearMap.zero_apply, sum_empty, range_eq_empty_of_isEmpty]
  · exact setToSimpleFunc_const' T x

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