setToFun_zero_left — Mathlib

English

If T is identically zero on all measurable finite μ-sets, then setToFun μ T hT f = 0 for any f.

Русский

Если T(s) = 0 для всех измеримых множеств s с конечной мерой μ, то setToFun(μ, T, hT, f) = 0.

LaTeX

$$$\forall f:\; (\forall s,\ MeasurableSet s \rightarrow μ s < ∞ \rightarrow T s = 0) \Rightarrow setToFun(\mu, T)\,h_T\,f = 0$$$

Lean4

@[simp]
theorem setToFun_zero_left {hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C} : setToFun μ 0 hT f = 0 :=
  by
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf]; exact L1.setToL1_zero_left hT _
  · exact setToFun_undef hT hf

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