iSup_eq_top

Mathlib.Topology.Sets.OpenCover

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.IsOpenCover.iSup_eq_top

English

Under an open cover, the supremum of the index-wise opens equals the top element.

Русский

При открытом покрытии супремум по индексу равен топу.

LaTeX

$$iSup_eq_top(hu) : ⨆ i, u i = ⊤$$

Lean4

theorem iSup_eq_top (hu : IsOpenCover u) : ⨆ i, u i = ⊤ :=
  hu

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

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

Разделы

Аффилиация

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