restrict_congr_meas — Mathlib

English

If s is measurable, then μ|_s = ν|_s iff μ and ν agree on all measurable subsets of s.

Русский

Если s измеримо, то μ|_s = ν|_s тогда и только тогда, когда μ и ν совпадают на всех измеримых подмножеств s.

LaTeX

$$$MeasurableSet\,s \Rightarrow (μ.restrict s = ν.restrict s \iff \forall t \subseteq s, MeasurableSet\,t \Rightarrow μ t = ν t)$$$

Lean4

theorem restrict_congr_meas (hs : MeasurableSet s) :
    μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → μ t = ν t :=
  ⟨fun H t hts ht => by rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht], fun H =>
    ext fun t ht => by rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]⟩

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