toTopologicalSpace_bot

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#UniformSpace.toTopologicalSpace_bot

English

The topology of the bottom uniform space is the bottom topology ( indiscrete ).

Русский

Топология нижнего равномерного пространства является нижней топологией (независимой).

LaTeX

$$toTopologicalSpace(⊥) = ⊥$$

Lean4

theorem toTopologicalSpace_bot : @UniformSpace.toTopologicalSpace α ⊥ = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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