bot_uniformity

Mathlib.Topology.UniformSpace.Basic

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

English

The bottom uniform space’s uniformity equals the principal filter on idRel.

Русский

Униформность нижнего пространства равна принципиальному фильтру idRel.

LaTeX

$$$𝓤[(⊥ : UniformSpace α)] = 𝓟 \mathrm{idRel}$$$

Lean4

theorem bot_uniformity : 𝓤[(⊥ : UniformSpace α)] = 𝓟 idRel :=
  rfl

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

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

Разделы

Аффилиация

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