countablySeparated_subtype_of_hasCountableSeparatingOn

English

If α is measurable and s has HasCountableSeparatingOn, then s is CountablySeparated.

Русский

Если у α есть HasCountableSeparatingOn на s, то s счетно разделено.

LaTeX

$$$ {\\alpha} [inst : MeasurableSpace \\alpha] {s : Set \\alpha} [h : HasCountableSeparatingOn \\alpha MeasurableSet s] : CountablySeparated s $$$

Lean4

instance countablySeparated_subtype_of_hasCountableSeparatingOn [MeasurableSpace α] {s : Set α}
    [h : HasCountableSeparatingOn _ MeasurableSet s] : CountablySeparated s :=
  CountablySeparated.subtype_iff.mpr h

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