Lean4
/-- Consider a real set `s`. If a property is true almost everywhere in `s ∩ (a, b)` for
all `a, b ∈ s`, then it is true almost everywhere in `s`. Formulated with bare membership.
See also `ae_restrict_of_ae_restrict_inter_Ioo`. -/
theorem ae_of_mem_of_ae_of_mem_inter_Ioo {μ : Measure ℝ} [NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop}
(h : ∀ a b, a ∈ s → b ∈ s → a < b → ∀ᵐ x ∂μ, x ∈ s ∩ Ioo a b → p x) : ∀ᵐ x ∂μ, x ∈ s → p x := by
/- By second-countability, we cover `s` by countably many intervals `(a, b)` (except maybe for
two endpoints, which don't matter since `μ` does not have any atom). -/
let T : s × s → Set ℝ := fun p => Ioo p.1 p.2
let u := ⋃ i : ↥s × ↥s, T i
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
obtain ⟨A, A_count, hA⟩ : ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
isOpen_iUnion_countable _ fun p => isOpen_Ioo
have M : ∀ᵐ x ∂μ, x ∉ s \ u := hfinite.countable.ae_notMem _
have M' : ∀ᵐ x ∂μ, ∀ (i : ↥s × ↥s), i ∈ A → x ∈ s ∩ T i → p x :=
by
rw [ae_ball_iff A_count]
rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
rcases le_or_gt b a with (hba | hab)
· simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true, mem_empty_iff_false]
· exact h a b as bs hab
filter_upwards [M, M'] with x hx h'x
intro xs
by_cases Hx : x ∈ ⋃ i : ↥s × ↥s, T i
· rw [← hA] at Hx
obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
apply h'x p pA ⟨xs, xp⟩
· exact False.elim (hx ⟨xs, Hx⟩)
