iInf

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#R1Space.iInf

← MathLib Explorer

English

The indexed infimum of a family of R1 spaces is again an R1 space.

Русский

Индексированное инфимумное объединение семей R1-пространств образует R1-пространство.

LaTeX

$$R1Space(iInf t)$$

Lean4

protected theorem iInf {ι X : Type*} {t : ι → TopologicalSpace X} (ht : ∀ i, @R1Space X (t i)) : @R1Space X (iInf t) :=
  .sInf <| forall_mem_range.2 ht

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

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

Разделы

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

Аффилиация

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