English
The Lusin separation theorem states that two disjoint analytic sets can be separated by disjoint Borel sets.
Русский
Теорема Лусина о разделимости: два непересекающихся аналитических множества можно разделить непересекающимися борелевыми множествами.
LaTeX
$$$\text{AnalyticSet}(s) \land \text{AnalyticSet}(t) \land Disjoint(s,t) \Rightarrow \text{MeasurablySeparable}(s,t).$$$
Lean4
/-- The **Lusin separation theorem**: if two analytic sets are disjoint, then they are contained in
disjoint Borel sets. -/
theorem measurablySeparable [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {s t : Set α} (hs : AnalyticSet s)
(ht : AnalyticSet t) (h : Disjoint s t) : MeasurablySeparable s t :=
by
rw [AnalyticSet] at hs ht
rcases hs with (rfl | ⟨f, f_cont, rfl⟩)
· refine ⟨∅, Subset.refl _, by simp, MeasurableSet.empty⟩
rcases ht with (rfl | ⟨g, g_cont, rfl⟩)
· exact ⟨univ, subset_univ _, by simp, MeasurableSet.univ⟩
exact measurablySeparable_range_of_disjoint f_cont g_cont h
