isOpen_sUnion

Mathlib.Topology.Defs.Basic

URI: https://scilib.ai/kg/mathlib#isOpen_sUnion

English

The union of an arbitrary family of open sets is open.

Русский

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

LaTeX

$$$\forall t\in s,\ IsOpen(t) \Rightarrow \IsOpen(\bigcup s)$$$

Lean4

theorem isOpen_sUnion {s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) :=
  TopologicalSpace.isOpen_sUnion s h

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

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

Разделы

Аффилиация

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