exists_mem

Mathlib.Topology.Sets.OpenCover

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

English

If u is an open cover, every point a ∈ X lies in some u_i.

Русский

Если u — открытое покрытие, то любой пункт пространства принадлежит хотя бы одному u_i.

LaTeX

$$exists_mem (hu : IsOpenCover u) (a : X) : ∃ i, a ∈ u i$$

Lean4

theorem exists_mem (hu : IsOpenCover u) (a : X) : ∃ i, a ∈ u i := by simpa [← hu.iSup_set_eq_univ] using mem_univ a

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

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

Разделы

Аффилиация

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