restrict_toMeasurable — Mathlib

English

If countable index set ι and s_i are pairwise disjoint, then equality of restrictions on each s_i implies equality on the union restriction.

Русский

Если счетное множество индексов ι и s_i попарно непересекаются, то равенство ограничений на каждом s_i эквивалентно равенству ограничения на объединение.

LaTeX

$$$[Countable\, ι] \ (Pairwise\, Disjoint\, on\, s) \Rightarrow (\mu.restrict (\bigcup i, s i) = \nu.restrict (\bigcup i, s i) \iff \forall i, \mu.restrict (s i) = \nu.restrict (s i))$$$

Lean4

theorem restrict_toMeasurable (h : μ s ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s :=
  ext fun t ht => by rw [restrict_apply ht, restrict_apply ht, inter_comm, measure_toMeasurable_inter ht h, inter_comm]

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