isLindelof

Mathlib.Topology.Compactness.Lindelof

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

English

If s is hereditarily Lindelöf, then s is Lindelöf.

Русский

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

LaTeX

$$$\\text{If } hs: IsHereditarilyLindelof(s), \\; IsLindelof(s).$$$

Lean4

theorem isLindelof (hs : IsHereditarilyLindelof s) : IsLindelof s :=
  hs.isLindelof_subset Subset.rfl

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

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

Разделы

Аффилиация

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