ext_iff_of_biUnion_eq_univ — Mathlib

English

Two measures are equal iff their restrictions on all s_i with i in a countable index set are equal, provided ⋃ i∈S s_i = univ.

Русский

Две меры равны тогда и только тогда, когда их ограничения на все s_i с i в счётном индексе равны, если ⋃ i∈S s_i = univ.

LaTeX

$$$[Countable\, ι] \ (\text{hs : } \bigcup_{i} s_i = univ) \Rightarrow (μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) \iff ∀ i, μ.restrict (s i) = ν.restrict (s i))$$$

Lean4

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

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