measurableSingletonClass_of_countablySeparated

English

If a space is countably separated, it has a MeasurableSingletonClass.

Русский

Если пространство имеет счетчивое разделение, оно имеет MeasurableSingletonClass.

LaTeX

$$$ [MeasurableSpace \\alpha] [CountablySeparated \\alpha] : MeasurableSingletonClass \\alpha $$$

Lean4

theorem measurableSingletonClass_of_countablySeparated [MeasurableSpace α] [CountablySeparated α] :
    MeasurableSingletonClass α :=
  by
  rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩
  refine ⟨fun x ↦ ?_⟩
  rw [← finj.preimage_image { x }, image_singleton]
  exact fmeas <| MeasurableSet.singleton _

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