ae true in volume.restrict

Stream: Is there code for X?

[Alex Kontorovich]

I know that something is true for all elements of a set s, and want to know that it's true ae w.r.t. a measure restricted to s. So what's the right lemma to use here?

import Mathlib.MeasureTheory.Measure.Haar.OfBasis

open MeasureTheory

example (s : Set ℝ) (P : ℝ → Prop) (hP : ∀ x ∈ s, P x) :
    ∀ᵐ (x : ℝ) ∂(volume.restrict s), P x := by
  filter_upwards [MeasureTheory.self_mem_ae_restrict sorry]
  exact hP

MeasureTheory.self_mem_ae_restrict requires measurability (which I would rather avoid trying to prove in my context). Isn't the statement even true without assuming measurability? Thanks for your help!

[Yury G. Kudryashov]

You need measurability of s or {x | P x} for this to be true.

[Vincent Beffara]

Yes otherwise the relevant set on which hP needs to hold is toMeasurable volume s which might be much bigger.

[Vincent Beffara]

E.g. docs#MeasureTheory.Measure.restrict_toMeasurable