subtype_iff — Mathlib

English

For any set s, CountablySeparated s is equivalent to HasCountableSeparatingOn α MeasurableSet s.

Русский

Для подмножества s верно: CountablySeparated s эквивалентно HasCountableSeparatingOn α MeasurableSet s.

LaTeX

$$$ [MeasurableSpace α] {s : Set α} : CountablySeparated s \\iff HasCountableSeparatingOn α MeasurableSet s $$$

Lean4

theorem subtype_iff [MeasurableSpace α] {s : Set α} :
    CountablySeparated s ↔ HasCountableSeparatingOn α MeasurableSet s :=
  by
  rw [countablySeparated_def]
  exact HasCountableSeparatingOn.subtype_iff

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