English
Let s and t be measurable sets on a measure space such that s and t are equal almost everywhere with respect to μ. Then for every predicate p : α → Prop, p holds almost everywhere on s with respect to μ if and only if p holds almost everywhere on t with respect to μ.
Русский
Пусть s и t — измеримые множества на измеримое пространство с мерой μ, причём они равны почти всюду относительно μ. Тогда для любого предиката p : α → истина верна почти всюду на s по μ тогда и только тогда, когда p верно почти всюду на t по μ.
LaTeX
$$$ (s =^{\mu}_{ae} t) \rightarrow \forall p : \alpha \to \mathrm{Prop}, \big(\forall^{\mathrm{a.e.}} x \partial \mu.restrict s, p(x)\big) \iff \big(\forall^{\mathrm{a.e.}} x \partial \mu.restrict t, p(x)\big) $$$
Lean4
/-- If two measurable sets are ae_eq then any proposition that is almost everywhere true on one
is almost everywhere true on the other -/
theorem ae_restrict_congr_set {s t} (hst : s =ᵐ[μ] t) {p : α → Prop} :
(∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ.restrict t, p x :=
⟨ae_restrict_of_ae_eq_of_ae_restrict hst, ae_restrict_of_ae_eq_of_ae_restrict hst.symm⟩
