setToSimpleFunc_zero_apply — Mathlib

English

If the zero simple function is fed into setToSimpleFunc with any T, the result is the zero element in the codomain. This is a simple consistency property of setToSimpleFunc on the zero function.

Русский

Если нулевая простая функция подается в setToSimpleFunc, результат равен нулю в кодом пространства.

LaTeX

$$$\forall \alpha, F, F', m, T:\ setToSimpleFunc T (0 : \alpha \to_{s} F) = 0$$$

Lean4

@[simp]
theorem setToSimpleFunc_zero_apply {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') :
    setToSimpleFunc T (0 : α →ₛ F) = 0 := by cases isEmpty_or_nonempty α <;> simp [setToSimpleFunc]

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