setToFun_zero_left' — Mathlib

English

Same principle as above with the same conclusion, expressed for a variant presentation.

Русский

То же самое утверждение, представленное иначе.

LaTeX

$$$\forall T\ hT\, \big( \forall s, MeasurableSet s \rightarrow μ s < ∞ \rightarrow T s = 0 \big) \Rightarrow setToFun(μ, T)\,hT\,f = 0$$$

Lean4

theorem setToFun_zero_left' (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0) :
    setToFun μ T hT f = 0 := by
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf]; exact L1.setToL1_zero_left' hT h_zero _
  · exact setToFun_undef hT hf

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