English
If every x in s has s as a right neighborhood of x, then s is measurable.
Русский
Если для каждого x∈s множества s является правой окрестностью x, то s измеримо.
LaTeX
$$∀ x ∈ s, s ∈ 𝓝[> ] x → MeasurableSet s$$
Lean4
/-- If a set is a right-neighborhood of all of its points, then it is measurable. -/
theorem of_mem_nhdsGT {s : Set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x) : MeasurableSet s :=
by
by_cases H : ∃ x ∈ s, IsTop x
· rcases H with ⟨x₀, x₀s, h₀⟩
have : s = { x₀ } ∪ s \ { x₀ } := by rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
rw [this]
refine (measurableSet_singleton _).union ?_
have A : ∀ x ∈ s \ { x₀ }, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
refine .of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩
obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s := (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)
refine (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, ?_⟩⟩
exact ne_of_lt (hy.2.trans_le (h₀ _))
· refine .of_mem_nhdsGT_aux h ?_
simp only [IsTop] at H
push_neg at H
exact H
