setToFun_zero — Mathlib

English

If the second argument is the zero operator (0), then setToFun evaluates to zero for any f.

Русский

Если Т равен нулю как оператор, то setToFun(μ, 0, hT, f) = 0 для любого f.

LaTeX

$$$\forall f:\; \mathrm{setToFun}(\mu, 0)\,h_T\,f = 0$$$

Lean4

@[simp]
theorem setToFun_zero (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT (0 : α → E) = 0 :=
  by
  rw [Pi.zero_def, setToFun_eq hT (integrable_zero _ _ _)]
  simp only [← Pi.zero_def]
  rw [Integrable.toL1_zero, ContinuousLinearMap.map_zero]

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