of_iUnion_nonneg — Mathlib

English

If every v(f_i) ≥ 0, then v(⋃ f_i) ≥ 0.

Русский

Если каждый v(f_i) ≥ 0, то v(⋃ f_i) ≥ 0.

LaTeX

$$0 ≤ v(⋃ i, f i)$$

Lean4

theorem of_iUnion_nonneg {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M]
    [OrderClosedTopology M] {v : VectorMeasure α M} (hf₁ : ∀ i, MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f))
    (hf₃ : ∀ i, 0 ≤ v (f i)) : 0 ≤ v (⋃ i, f i) :=
  (v.of_disjoint_iUnion hf₁ hf₂).symm ▸ tsum_nonneg hf₃

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