setToL1S — Mathlib

English

Let T assign to each measurable subset s of α a continuous linear map T(s): E → F. Then setToL1S extends T to the L1-simple-function space by evaluating on the simple representative of f: setToL1S(T)(f) := (toSimpleFunc f).setToSimpleFunc(T).

Русский

Пусть для каждой измеримой подмножества s ⊆ α задан непрерывно-линейный отображение T(s): E → F. Тогда расширение setToL1S(T) до пространства α →₁ₛ[μ] E определяется как setToL1S(T)(f) := (toSimpleFunc f).setToSimpleFunc(T).

LaTeX

$$$$\mathrm{setToL1S}(T)(f) = \big(\mathrm{toSimpleFunc}(f)\big).\mathrm{setToSimpleFunc}(T).$$$$

Lean4

/-- Extend `Set α → (E →L[ℝ] F')` to `(α →₁ₛ[μ] E) → F'`. -/
def setToL1S (T : Set α → E →L[ℝ] F) (f : α →₁ₛ[μ] E) : F :=
  (toSimpleFunc f).setToSimpleFunc T

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