isOpen

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhdsOf.isOpen

English

For every open neighborhood U of x, the underlying set is open.

Русский

Для каждой открытой окрестности U x множество U является открытым.

LaTeX

$$$\\\\forall U : \\\\mathrm{OpenNhdsOf}(x),\\\\ \\\\mathrm{IsOpen}((U : Set\\\\,\\\\alpha)).$$$

Lean4

protected theorem isOpen (U : OpenNhdsOf x) : IsOpen (U : Set α) :=
  U.is_open'

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

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

Разделы

Аффилиация

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