of_iUnion_nonpos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_iUnion_nonpos {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, v (f i) ≤ 0) : v (⋃ i, f i) ≤ 0 :=
  (v.of_disjoint_iUnion hf₁ hf₂).symm ▸ tsum_nonpos hf₃

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