Theorems · Theorem · measure theory

MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated

∀ (α : Type u_1) [inst : MeasurableSpace α] [MeasurableSpace.CountablySeparated α],
  ∃ f, Measurable f ∧ Function.Injective f

If a measurable space admits a countable sequence of measurable sets separating points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

Defined in

Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace.CountablySeparated