measurable_injection_nat_bool_of_countablySeparated

English

There exists a measurable injection from α into the Cantor space under countable separation.

Русский

Существует измеримое вложение из α в канторово пространство при счетном разделении.

LaTeX

$$$\\exists f: \\alpha \\to (\\mathbb{N} \\to Bool), Measurable f \\land Injective f$$$

Lean4

/-- 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). -/
theorem measurable_injection_nat_bool_of_countablySeparated [MeasurableSpace α] [CountablySeparated α] :
    ∃ f : α → ℕ → Bool, Measurable f ∧ Injective f :=
  by
  rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
  refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩
  exact (measurable_mapNatBool _).mono m'le le_rfl

Похожие утверждения