eq_zero_of_measure_zero — Mathlib

English

If a DominatedFinMeasAdditive relation holds, then the value on a measurable set s is zero whenever the measure of s is zero.

Русский

Если выполняется доминированная FinMeasAdditive, то T(s)=0 при μ(s)=0

LaTeX

$$T s = 0$$

Lean4

theorem eq_zero_of_measure_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ}
    (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hs_zero : μ s = 0) : T s = 0 :=
  by
  refine norm_eq_zero.mp ?_
  refine ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq ?_)).antisymm (norm_nonneg _)
  rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]

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