ae_of_ae_trim — Mathlib

English

If a property holds almost everywhere with respect to μ.trim hm, then it holds almost everywhere with respect to μ.

Русский

Если свойство выполняется почти всюду относительно μ.trim hm, то оно выполняется почти всюду относительно μ.

LaTeX

$$$(\\text{ae}(μ.trim hm))(P) \\Rightarrow (\\text{ae}(μ))(P).$$$

Lean4

theorem ae_of_ae_trim (hm : m ≤ m0) {μ : Measure α} {P : α → Prop} (h : ∀ᵐ x ∂μ.trim hm, P x) : ∀ᵐ x ∂μ, P x :=
  measure_eq_zero_of_trim_eq_zero hm h

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