English
A set function is FinMeasAdditive if on the union of two disjoint measurable sets with finite measure its value is the sum of the values on each set.
Русский
Наборная функция имеет конечную аддитивность: на объединении двух непересекающихся измеримых множеств с конечной мерой значение равно сумме значений на каждом множестве.
LaTeX
$$\forall s,t,\ MeasurableSet(s)\,\&\, MeasurableSet(t)\,\&\ μ s ≠ ∞ \&\ μ t ≠ ∞ \&\ Disjoint s t \Rightarrow T(s\cup t)=T(s)+T(t)$$
Lean4
/-- A set function is `FinMeasAdditive` if its value on the union of two disjoint measurable
sets with finite measure is the sum of its values on each set. -/
def FinMeasAdditive {β} [AddMonoid β] {_ : MeasurableSpace α} (μ : Measure α) (T : Set α → β) : Prop :=
∀ s t, MeasurableSet s → MeasurableSet t → μ s ≠ ∞ → μ t ≠ ∞ → Disjoint s t → T (s ∪ t) = T s + T t
