ae_mem_of_ae_add_linearMap_mem — Mathlib

English

If a property holds almost everywhere after adding a translate by y to Lx, it holds almost everywhere in y.

Русский

Если свойство почти везде сохраняется после добавления y к Lx, то оно почти везде и в y.

LaTeX

$$ae_mem_of_ae_add_linearMap_mem hs h : ∀ᵐ y ∂ν, y ∈ s$$

Lean4

/-- To check that a property holds almost everywhere with respect to an additive Haar measure, it
suffices to check it almost everywhere along all translates of a given vector subspace. This is an
instance of a disintegration argument for additive Haar measures. -/
theorem ae_mem_of_ae_add_linearMap_mem [LocallyCompactSpace F] {s : Set F} (hs : MeasurableSet s)
    (h : ∀ y, ∀ᵐ x ∂μ, y + L x ∈ s) : ∀ᵐ y ∂ν, y ∈ s :=
  (ae_ae_add_linearMap_mem_iff L μ ν hs).1 (Filter.Eventually.of_forall h)

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