coe_iSup

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.coe_iSup

English

The underlying set of iSup s equals the union over i of the underlying sets s i.

Русский

Обоснование iSup: множество, соответствующее iSup s, равно объединению множеств s i.

LaTeX

$$$ (↑(iSup \! s) : Set α) = \bigcup_i (↑(s i)) $$$

Lean4

@[simp, norm_cast]
theorem coe_iSup {ι} (s : ι → Opens α) : ((⨆ i, s i : Opens α) : Set α) = ⋃ i, s i := by simp [iSup]

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

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

Разделы

Аффилиация

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