Theorems · Theorem · general topology

MeasureTheory.AnalyticSet.measurablySeparable

∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] [inst_2 : MeasurableSpace α] [OpensMeasurableSpace α]
  {s t : Set α},
  MeasureTheory.AnalyticSet s → MeasureTheory.AnalyticSet t → Disjoint s t → MeasureTheory.MeasurablySeparable s t

The Lusin separation theorem: if two analytic sets are disjoint, then they are contained in disjoint Borel sets.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

2 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT2SpaceMeasurableSpaceOpensMeasurableSpace