ext_iff_of_iUnion_eq_univ — Mathlib

English

For [Countable ι], if s_i are pairwise disjoint in the sense of Disjoint on s, then the restricted union equals the iSup of the restricted pieces.

Русский

Для счётного множества индексов ι, если множества попарно дисжойнны, то ограничение объединения равно iSup ограничений по частям.

LaTeX

$$$[Countable\, ι] \ (Pairwise\, Disjoint\, on\, s) \implies \mu.restrict (\\bigcup i, s i) = \bigsqcup_i (\\mu.restrict (s i))$$$

Lean4

/-- Two measures are equal if they have equal restrictions on a spanning collection of sets
  (formulated using `Union`). -/
theorem ext_iff_of_iUnion_eq_univ [Countable ι] {s : ι → Set α} (hs : ⋃ i, s i = univ) :
    μ = ν ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i) := by
  rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]

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