setToFun_measure_zero' — Mathlib

English

If μ(S) = 0 for all measurable S from a family, then setToFun μ T hT f = 0.

Русский

Если мера множества S равна нулю для всех измеримых S, то setToFun равен нулю.

LaTeX

$$$\forall s: MeasurableSet, μ s = 0 \Rightarrow setToFun(μ, T) h_T f = 0$$$

Lean4

theorem setToFun_measure_zero' (hT : DominatedFinMeasAdditive μ T C) (h : ∀ s, MeasurableSet s → μ s < ∞ → μ s = 0) :
    setToFun μ T hT f = 0 :=
  setToFun_zero_left' hT fun s hs hμs => hT.eq_zero_of_measure_zero hs (h s hs hμs)

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