setToSimpleFunc_add_left — Mathlib

English

The operator setToSimpleFunc is additive in the left factor: applying add of two maps T and T' yields the sum of setToSimpleFunc applied to each, i.e., setToSimpleFunc (T+T') f = setToSimpleFunc T f + setToSimpleFunc T' f.

Русский

Оператор setToSimpleFunc аддитивен слева: применяя сумму отображений T и T' даёт равенство setToSimpleFunc (T+T') f = setToSimpleFunc T f + setToSimpleFunc T' f.

LaTeX

$$$ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f $$$

Lean4

theorem setToSimpleFunc_add_left {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] F') {f : α →ₛ F} :
    setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f :=
  by
  simp_rw [setToSimpleFunc, Pi.add_apply]
  push_cast
  simp_rw [Pi.add_apply, sum_add_distrib]

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