ae_restrict_neBot — Mathlib

English

If s and t are almost everywhere equal with respect to μ, then any property that holds a.e. on s also holds a.e. on t.

Русский

Если s и t равны почти всюду по μ, то свойство, выполняющееся почти наверху на s, выполняется и на t.

LaTeX

$$$\text{ae}(μ|_s) = \text{ae}(μ|_t) \Rightarrow (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ|_s) \Rightarrow (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ|_t).$$$

Lean4

theorem ae_restrict_neBot {s} : (ae <| μ.restrict s).NeBot ↔ μ s ≠ 0 :=
  neBot_iff.trans ae_restrict_eq_bot.not

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