isGenericPoint

Mathlib.Topology.Sober

URI: https://scilib.ai/kg/mathlib#genericPoints.isGenericPoint

English

A generic point x in genericPoints α is generic for its component: IsGenericPoint(x.1, (component x).1).

Русский

Генерирующая точка x в genericPoints α является генерирующей точкой для своего компонента.

LaTeX

$$$IsGenericPoint\\,(x.1)\\,(component(x)).1$$$

Lean4

theorem isGenericPoint (x : genericPoints α) : IsGenericPoint x.1 (component x).1 :=
  rfl

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

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

Разделы

Аффилиация

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