IsSigmaSubadditive — Mathlib

English

An additive content is sigma-subadditive if for any sequence of sets in C whose union is in C, m(union) ≤ sum m on the sequence.

Русский

Аддитивное содержательное множество является сигма-субаддитивным: для любой последовательности множеств из C, чьё объединение также в C, имеем неравенство

LaTeX

$$IsSigmaSubadditive m := ∀ ⦃f : ℕ → Set α⦄ (_hf : ∀ i, f i ∈ C) (_hf_Union : (⋃ i, f i) ∈ C), m (⋃ i, f i) ≤ ∑' i, m (f i)$$

Lean4

/-- An additive content is said to be sigma-sub-additive if for any sequence of sets `f` in `C` such
that `⋃ i, f i ∈ C`, we have `m (⋃ i, f i) ≤ ∑' i, m (f i)`. -/
def IsSigmaSubadditive (m : AddContent C) : Prop :=
  ∀ ⦃f : ℕ → Set α⦄ (_hf : ∀ i, f i ∈ C) (_hf_Union : (⋃ i, f i) ∈ C), m (⋃ i, f i) ≤ ∑' i, m (f i)

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