restrict_sUnion_congr — Mathlib

English

If S is a countable set of sets, then μ|_{⋃ S} = ν|_{⋃ S} iff ∀ s ∈ S, μ|_s = ν|_s.

Русский

Если S — счётное множество множеств, то μ|_{⋃ S} = ν|_{⋃ S} тогда и только тогда, когда ∀ s ∈ S, μ|_s = ν|_s.

LaTeX

$$$S.Countable \implies (μ.restrict (\\bigcup S) = ν.restrict (\\bigcup S) \iff \forall s \in S, μ.restrict s = ν.restrict s)$$$

Lean4

theorem restrict_sUnion_congr {S : Set (Set α)} (hc : S.Countable) :
    μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s := by
  rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]

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