isOpen_empty

Mathlib.Topology.Basic

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

English

The empty set is open in any topology.

Русский

Пустое множество/open в любой топологии.

LaTeX

$$$IsOpen(\emptyset)$$$

Lean4

@[simp]
theorem isOpen_empty : IsOpen (∅ : Set X) := by rw [← sUnion_empty]; exact isOpen_sUnion fun a => False.elim

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

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

Разделы

Аффилиация

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