ae_restrict_of_ae_eq_of_ae_restrict

English

If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other.

Русский

Если два измеримых множества равны почти повсюду, то любая произвольная пропозиция, верная почти всё на одно, верна почти всё на другое.

LaTeX

$$$\text{ae}(μ) \EventuallyEq s t \Rightarrow (\forall p, \text{ae on } s \Rightarrow \text{ae on } t).$$$

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_of_ae_eq_of_ae_restrict {s t} (hst : s =ᵐ[μ] t) {p : α → Prop} :
    (∀ᵐ x ∂μ.restrict s, p x) → ∀ᵐ x ∂μ.restrict t, p x := by simp [Measure.restrict_congr_set hst]

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