isSeparable

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#Set.Countable.isSeparable

English

If s is countable, then s is separable.

Русский

Если множество счётно, то оно сепарабельно.

LaTeX

$$$s.Countable \rightarrow IsSeparable(s)$$$

Lean4

theorem _root_.Set.Countable.isSeparable {s : Set α} (hs : s.Countable) : IsSeparable s :=
  ⟨s, hs, subset_closure⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru