map_empty_eq_zero — Mathlib

English

If two maps are FinMeasAdditive, so is their sum map.

Русский

Если две отображения FinMeasAdditive, то их сумма также FinMeasAdditive.

LaTeX

$$hT.add hT' : FinMeasAdditive μ (T + T')$$

Lean4

theorem map_empty_eq_zero {β} [AddCancelMonoid β] {T : Set α → β} (hT : FinMeasAdditive μ T) : T ∅ = 0 :=
  by
  have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne
  specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)
  rw [Set.union_empty] at hT
  nth_rw 1 [← add_zero (T ∅)] at hT
  exact (add_left_cancel hT).symm

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