setToL1S_eq_setToSimpleFunc — Mathlib

English

For any T and f with f expressed via its simple representation, setToL1S(T)(f) equals applying setToSimpleFunc to the simple representation of f.

Русский

Для любых T и f справедливо: setToL1S(T)(f) равно применению setToSimpleFunc к простой записи f.

LaTeX

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

Lean4

theorem setToL1S_eq_setToSimpleFunc (T : Set α → E →L[ℝ] F) (f : α →₁ₛ[μ] E) :
    setToL1S T f = (toSimpleFunc f).setToSimpleFunc T :=
  rfl

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