Theorems · Theorem · general topology

MeasureTheory.measurablySeparable_range_of_disjoint

∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] [inst_2 : MeasurableSpace α] [OpensMeasurableSpace α]
  {f g : (ℕ → ℕ) → α},
  Continuous f →
    Continuous g → Disjoint (Set.range f) (Set.range g) → MeasureTheory.MeasurablySeparable (Set.range f) (Set.range g)

The hard part of the Lusin separation theorem saying that two disjoint analytic sets are contained in disjoint Borel sets (see the full statement in AnalyticSet.measurablySeparable). Here, we prove this when our analytic sets are the ranges of functions from ℕ → ℕ.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceMeasurableSpaceOpensMeasurableSpace