generateFrom_setOf_isOpen

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.generateFrom_setOf_isOpen

English

For any topology t on α, the topology generated by the collection of its open sets equals t.

Русский

Для любой топологии t на α топология, порождаемая множеством его открытых множеств, равна t.

LaTeX

$$$generateFrom\\;\\{s \\mid IsOpen[t] s\\} = t$$$

Lean4

theorem generateFrom_setOf_isOpen (t : TopologicalSpace α) : generateFrom {s | IsOpen[t] s} = t :=
  (gciGenerateFrom α).u_l_eq t

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

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

Разделы

Аффилиация

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