countablySeparated_def — Mathlib

English

CountablySeparated α holds iff there exists HasCountableSeparatingOn α MeasurableSet univ.

Русский

CountablySeparated α эквивалентно существованию HasCountableSeparatingOn α MeasurableSet univ.

LaTeX

$$$ CountablySeparated \\alpha \\iff HasCountableSeparatingOn \\alpha MeasurableSet univ $$$

Lean4

theorem countablySeparated_def [MeasurableSpace α] :
    CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet univ :=
  ⟨fun h ↦ h.countably_separated, fun h ↦ ⟨h⟩⟩

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