English
If every point of a set s has a right-neighborhood contained in s and every point of s has a larger point, then s is a measurable set.
Русский
Если для каждой точки множества s существует правая окрестность, содержащаяся в s, и для каждой точки s существует точка больше, то s измеримо.
LaTeX
$$$\\forall x\\in s,\\ s\\in \\mathcal{N}_{>}(x)\\quad\\land\\quad \\forall x\\in s,\\exists y>x\\quad\\Rightarrow\\quad \\text{MeasurableSet}(s)$$$
Lean4
theorem of_mem_nhdsGT_aux {s : Set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x) (h' : ∀ x ∈ s, ∃ y, x < y) : MeasurableSet s :=
by
choose! M hM using h'
suffices H : (s \ interior s).Countable
by
have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
rw [this]
exact isOpen_interior.measurableSet.union H.measurableSet
have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s := fun x hx => (mem_nhdsGT_iff_exists_Ioo_subset' (hM x hx)).1 (h x hx)
choose! y hy h'y using A
have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) :=
by
intro x hx x' hx' hxx'
rcases lt_or_gt_of_ne hxx' with (h' | h')
· refine disjoint_left.2 fun z hz h'z => ?_
have : x' ∈ interior s := mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
exact False.elim (hx'.2 this)
· refine disjoint_left.2 fun z hz h'z => ?_
have : x ∈ interior s := mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
exact False.elim (hx.2 this)
exact B.countable_of_Ioo fun x hx => hy x hx.1
