of_quasiSeparatedSpace

Mathlib.Topology.QuasiSeparated

URI: https://scilib.ai/kg/mathlib#IsQuasiSeparated.of_quasiSeparatedSpace

English

If α is a quasi-separated space, then any subset s ⊆ α is quasi-separated.

Русский

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

LaTeX

$$QuasiSeparatedSpace α ⇒ IsQuasiSeparated s$$

Lean4

theorem of_quasiSeparatedSpace (s : Set α) : IsQuasiSeparated s :=
  isQuasiSeparated_univ.of_subset (Set.subset_univ _)

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

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

Разделы

Аффилиация

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