countablySeparated — Mathlib

English

For any s, CountablySeparated s holds if α is CountablySeparated.

Русский

Для подмножества s верно, что CountablySeparated s, если пространство α счетно разделено.

LaTeX

$$$ CountablySeparated α \\Rightarrow CountablySeparated s $$$

Lean4

instance (priority := 100) countablySeparated [MeasurableSpace α] [h : CountablySeparated α] {s : Set α} :
    CountablySeparated s := by
  rw [CountablySeparated.subtype_iff]
  exact h.countably_separated.mono (fun s ↦ id) <| subset_univ _

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