instTopUniformSpace

Mathlib.Topology.UniformSpace.Basic

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

Lean4

instance : Top (UniformSpace α) :=
  ⟨@UniformSpace.mk α ⊤ ⊤ le_top le_top fun x ↦ by simp only [nhds_top, comap_top]⟩

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

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

Разделы

Аффилиация

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