extend_iUnion_nat — Mathlib

English

For a family of sets indexed by N with disjointness, the extension over the union equals the sum of extensions: extend m (⋃ i, f i) = ∑' i, extend m (f i).

Русский

Для семейства множеств, индексируемого по естественным числам, где множества попарно беспересекаются, расширение по объединению равно сумме расширений: extend m (⋃ i, f i) = ∑' i, extend m (f i).

LaTeX

$$$\\mathrm{extend}\\, m\\ (\\bigcup_{i} f_i) = \\sum_{i}^{\\prime} \\mathrm{extend}\\, m\\ (f_i)$$$

Lean4

theorem extend_iUnion_nat {f : ℕ → Set α} (hm : ∀ i, P (f i)) (mU : m (⋃ i, f i) (PU hm) = ∑' i, m (f i) (hm i)) :
    extend m (⋃ i, f i) = ∑' i, extend m (f i) :=
  (extend_eq _ _).trans <|
    mU.trans <| by
      congr with i
      rw [extend_eq]

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