mono

Mathlib.Topology.Bases

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

← MathLib Explorer

English

If s is separable and u ⊆ s, then u is separable.

Русский

Если s сепарабельно и u ⊆ s, то u сепарабельно.

LaTeX

$$$IsSeparable(s) \rightarrow (u \subseteq s) \rightarrow IsSeparable(u)$$$

Lean4

theorem mono {s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u :=
  by
  rcases hs with ⟨c, c_count, hs⟩
  exact ⟨c, c_count, hu.trans hs⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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