mem

Mathlib.Topology.Sets.Opens

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

English

Let x be a point in a topological space and U an open neighborhood of x. Then x ∈ U.

Русский

Пусть x — точка в топологическом пространстве и U — открытая окрестность x. Тогда x ∈ U.

LaTeX

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

Lean4

protected theorem mem (U : OpenNhdsOf x) : x ∈ U :=
  U.mem'

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

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

Разделы

Аффилиация

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