instTopologicalSpaceSignType

Mathlib.Topology.Instances.Sign

URI: https://scilib.ai/kg/mathlib#instTopologicalSpaceSignType

English

The topology on SignType is the indiscrete (bottom) topology.

Русский

Топология на SignType — индиcкретная (нижняя) топология.

LaTeX

$$$\\mathcal{T}_{\\mathrm{SignType}} = \\bot.$$$

Lean4

instance : TopologicalSpace SignType :=
  ⊥

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

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

Разделы

Аффилиация

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