ext_iff_of_sUnion_eq_univ — Mathlib

English

Two measures are equal if they have equal restrictions on a spanning collection of sets given by a countable S of sets whose sUnion equals univ.

Русский

Две меры равны, если их ограничения по счётному набору множеств, покрывающих всe множество, совпадают.

LaTeX

$$$[Countable\, S] (\bigcup S = univ) \Rightarrow (μ = ν \iff ∀ s ∈ S, μ.restrict s = ν.restrict s)$$$

Lean4

/-- Two measures are equal if they have equal restrictions on a spanning collection of sets
  (formulated using `sUnion`). -/
theorem ext_iff_of_sUnion_eq_univ {S : Set (Set α)} (hc : S.Countable) (hs : ⋃₀ S = univ) :
    μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s :=
  ext_iff_of_biUnion_eq_univ hc <| by rwa [← sUnion_eq_biUnion]

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