union

Mathlib.Topology.Basic

URI: https://scilib.ai/kg/mathlib#IsOpen.union

English

The union of two open sets is open.

Русский

Объединение двух открытых множеств открыто.

LaTeX

$$$IsOpen\,s_1 \to IsOpen\,s_2 \to IsOpen\,(s_1 \cup s_2)$$$

Lean4

theorem union (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂) := by rw [union_eq_iUnion];
  exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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

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

Разделы

Аффилиация

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