hasCountableSeparatingOn_of_countablySeparated_subtype

English

If α is measurable and there is a CountablySeparated instance on s, then HasCountableSeparatingOn _ MeasurableSet s.

Русский

Если α измеримо и на подмножестве s существует счетчивое разделение, то у s имеется HasCountableSeparatingOn.

LaTeX

$$$ [MeasurableSpace α] {s : Set α} [h : CountablySeparated s] : HasCountableSeparatingOn _ MeasurableSet s $$$

Lean4

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

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