extend_iUnion — Mathlib

English

If P s1 holds and s1 ⊆ s2, then extend m s1 ≤ extend m s2.

Русский

Если P s1 выполняется и s1 ⊆ s2, то extend m s1 ≤ extend m s2.

LaTeX

$$$P s_1 \\Rightarrow s_1 \\subseteq s_2 \\Rightarrow \\mathrm{extend}\\, m\\ s_1 \\le \\mathrm{extend}\\, m\\ s_2$$$

Lean4

theorem extend_iUnion {β} [Countable β] {f : β → Set α} (hd : Pairwise (Disjoint on f)) (hm : ∀ i, P (f i)) :
    extend m (⋃ i, f i) = ∑' i, extend m (f i) :=
  by
  cases nonempty_encodable β
  rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]
  ·
    exact
      extend_iUnion_nat PU (fun n => Encodable.iUnion_decode₂_cases P0 hm)
        (mU _ (Encodable.iUnion_decode₂_disjoint_on hd))
  · exact extend_empty P0 m0

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