iSup_set_eq_univ

Mathlib.Topology.Sets.OpenCover

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

English

The union of the underlying sets of an open cover equals the universe.

Русский

Объединение базисных множеств открытого покрытия равно вселенной.

LaTeX

$$$⋃ i, (u i : Set X) = univ$$$

Lean4

theorem iSup_set_eq_univ (hu : IsOpenCover u) : ⋃ i, (u i : Set X) = univ := by
  simpa [← SetLike.coe_set_eq] using hu.iSup_eq_top

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

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

Разделы

Аффилиация

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