isLindelof_subset

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#IsHereditarilyLindelof.isLindelof_subset

English

If s is hereditarily Lindelöf and t ⊆ s, then t is Lindelöf.

Русский

Если s наследовательно Линдельфово и t ⊆ s, то t Линдельфово.

LaTeX

$$$\\text{If } hs: IsHereditarilyLindelof(s) \\text{ and } ht: t \\subseteq s, \\ text{ then } IsLindelof(t).$$$

Lean4

theorem isLindelof_subset (hs : IsHereditarilyLindelof s) (ht : t ⊆ s) : IsLindelof t :=
  hs t ht

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

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

Разделы

Аффилиация

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