English
There exists an open set u such that μ.everywherePosSubset s = s \\ u.
Русский
Существует открытое множество u такое, что μ.everywherePosSubset s = s \\ u.
LaTeX
$$$$ \\exists u\\text{ открытое}:\\mathcal{X},\\ \\mu.everywherePosSubset s = s \\setminus u. $$$$
Lean4
/-- The everywhere positive subset of a set is obtained by removing an open set. -/
theorem exists_isOpen_everywherePosSubset_eq_diff (μ : Measure α) (s : Set α) :
∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u :=
by
refine ⟨{x | ∃ n ∈ 𝓝[s] x, μ n = 0}, ?_, by ext x; simp [everywherePosSubset, zero_lt_iff]⟩
rw [isOpen_iff_mem_nhds]
intro x ⟨n, ns, hx⟩
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 ns with ⟨v, vx, hv⟩
rcases mem_nhds_iff.1 vx with ⟨w, wv, w_open, xw⟩
have A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} := by
intro y yw
refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
rw [inter_comm]
exact (inter_subset_inter_left _ wv).trans hv
have B : w ∈ 𝓝 x := w_open.mem_nhds xw
exact mem_of_superset B A
