isSeparable_closure

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.isSeparable_closure

English

IsSeparable (closure s) is equivalent to IsSeparable s.

Русский

IsSeparable(closure s) эквивалентно IsSeparable s.

LaTeX

$$$IsSeparable(closure\ s) \iff IsSeparable(s)$$$

Lean4

@[simp]
theorem isSeparable_closure : IsSeparable (closure s) ↔ IsSeparable s := by
  simp only [IsSeparable, isClosed_closure.closure_subset_iff]

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

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

Разделы

Аффилиация

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