measure_biUnion_lt_top — Mathlib

English

Let s be a finite index set and f: s → Set α be a family of sets such that μ(f(i)) < ∞ for all i ∈ s. Then μ(⋃_{i∈s} f(i)) < ∞.

Русский

Пусть s является конечным множителем индексов, и задана функция f: s → Set α такая, что μ(f(i)) < ∞ для всех i ∈ s. Тогда μ( ⋃_{i ∈ s} f(i) ) < ∞.

LaTeX

$$$\Big( card(s) < \infty \;\land\; \forall i \in s,\; \mu(f(i)) < \infty \Big) \Rightarrow \mu\Bigl(\bigcup_{i \in s} f(i)\Bigr) < \infty.$$$

Lean4

theorem measure_biUnion_lt_top {s : Set β} {f : β → Set α} (hs : s.Finite) (hfin : ∀ i ∈ s, μ (f i) < ∞) :
    μ (⋃ i ∈ s, f i) < ∞ :=
  by
  convert (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3
  · ext
    rw [Finite.mem_toFinset]
  · simpa only [ENNReal.sum_lt_top, Finite.mem_toFinset]

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