restrict_toMeasurable_of_cover — Mathlib

English

Let μ be a measure on α. If a set s is contained in a countable union of sets v_n and every intersection s ∩ v_n has finite μ-measure, then μ restricted to the measurable hull of s equals μ restricted to s.

Русский

Пусть μ — мера на α. Если множество s содержится в счётном объединении множеств v_n и для каждого n мера μ(s ∩ v_n) конечна, то ограничение μ на измеримое сверху s совпадает с ограничением на s.

LaTeX

$$$\bigl(s \subseteq \bigcup_{n} v_n\bigr) \land \bigl(\forall n, μ(s \cap v_n) \neq \infty\bigr) \Rightarrow μ|_{toMeasurable μ s} = μ|_s$$$

Lean4

theorem restrict_toMeasurable_of_cover {s : Set α} {v : ℕ → Set α} (hv : s ⊆ ⋃ n, v n) (h'v : ∀ n, μ (s ∩ v n) ≠ ∞) :
    μ.restrict (toMeasurable μ s) = μ.restrict s :=
  ext fun t ht => by simp only [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_cover ht hv h'v]

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