self_mem_principalOpen

Mathlib.Topology.Sheaves.Alexandrov

URI: https://scilib.ai/kg/mathlib#Alexandrov.self_mem_principalOpen

English

For every x in X, x belongs to its principal open: x ∈ principalOpen(x).

Русский

Для каждого x ∈ X выполняется x ∈ principalOpen(x).

LaTeX

$$$x \in \operatorname{principalOpen}(x)$$$

Lean4

theorem self_mem_principalOpen (x : X) : x ∈ principalOpen x :=
  le_refl _

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

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

Разделы

Аффилиация

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