totallySeparatedSpace — Mathlib

English

If s is a countable subset of a space X, then the subspace s inherits a totally separated topology.

Русский

Если s — счётное подмножество пространства X, то подпространство s имеет полностью раздельную топологию.

LaTeX

$$$s \\text{ countable } \\Rightarrow \\text{TotallySeparatedSpace } s$ (as a subtype).$$

Lean4

protected theorem _root_.Set.Countable.totallySeparatedSpace {s : Set X} (h : s.Countable) : TotallySeparatedSpace s :=
  have : _root_.Countable s := h
  inferInstanceAs (TotallySeparatedSpace s)

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