eq_zero — Mathlib

English

If a dominated FinMeasAdditive relation holds with zero bound, the value is zero.

Русский

Если граница равна нулю, результат равен нулю.

LaTeX

$$DominatedFinMeasAdditive μ T 0$$

Lean4

theorem eq_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} {_ : MeasurableSpace α}
    (hT : DominatedFinMeasAdditive (0 : Measure α) T C) {s : Set α} (hs : MeasurableSet s) : T s = 0 :=
  eq_zero_of_measure_zero hT hs (by simp only [Measure.coe_zero, Pi.zero_apply])

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