instTopologicalSpace

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#OrderDual.instTopologicalSpace

English

For any topological space X, the order dual Xᵒᵈ is equipped with the same topology as X.

Русский

Для любой топологической множества X двойственный по порядку Xᵒᵈ оснащается такой же топологией, как и X.

LaTeX

$$$ \\mathcal{T}_{X^{\\mathrm{op}}} = \\mathcal{T}_{X}. $$$

Lean4

instance instTopologicalSpace : TopologicalSpace Xᵒᵈ :=
  ‹_›

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

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

Разделы

Аффилиация

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