of_separableSpace

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.IsSeparable.of_separableSpace

English

If α is a separable space, then any subset s ⊆ α is separable in α.

Русский

Если пространство α сепарабельно, то любое подмножество s ⊆ α сепарабельно в α.

LaTeX

$$[SeparableSpace α] → ∀ s ⊆ α, IsSeparable s$$

Lean4

theorem of_separableSpace [h : SeparableSpace α] (s : Set α) : IsSeparable s :=
  IsSeparable.mono (isSeparable_univ_iff.2 h) (subset_univ _)

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

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

Разделы

Аффилиация

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