setToSimpleFunc — Mathlib

English

Extend Set α → F →L[ℝ] F' to (α →ₛ F) → F'.

Русский

Расширение отображения из множеств в линейные отображения по простым функциям.

LaTeX

$$def setToSimpleFunc (T) (f) : F' := ∑ x ∈ f.range, T (f ⁻¹' { x }) x$$

Lean4

/-- Extend `Set α → (F →L[ℝ] F')` to `(α →ₛ F) → F'`. -/
def setToSimpleFunc {_ : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : α →ₛ F) : F' :=
  ∑ x ∈ f.range, T (f ⁻¹' { x }) x

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