countablySeparated_of_hasCountableSeparatingOn

English

If α is a measurable space and there exists a countable separating family on α on the whole space, then α is CountablySeparated.

Русский

Если α— измеримое пространство и существует счетная семейство множеств, разделяющих точки на всем пространстве, то α является CountablySeparated.

LaTeX

$$$ [\\text{MeasurableSpace } \\alpha] [\\text{HasCountableSeparatingOn } \\alpha \\ MeasurableSet \\ univ] \\Rightarrow CountablySeparated \\alpha $$$

Lean4

instance countablySeparated_of_hasCountableSeparatingOn [MeasurableSpace α]
    [h : HasCountableSeparatingOn α MeasurableSet univ] : CountablySeparated α :=
  ⟨h⟩

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