of_subset

Mathlib.Topology.QuasiSeparated

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

← MathLib Explorer

English

If t is quasi-separated and s ⊆ t, then s is quasi-separated.

Русский

Если t квазиразделимо и s ⊆ t, то s тоже квазиразделимо.

LaTeX

$$IsQuasiSeparated t \\rightarrow (s \\subseteq t) \\rightarrow IsQuasiSeparated s$$

Lean4

theorem of_subset {s t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) : IsQuasiSeparated s :=
  by
  intro U V hU hU' hU'' hV hV' hV''
  exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

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

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

Разделы

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

Аффилиация

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