refl_le_uniformity

Mathlib.Topology.UniformSpace.Defs

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

English

The diagonal principal filter is below the uniformity.

Русский

Диагональная насчитывающая фильтр под равномерностью.

LaTeX

$$$\\mathcal{P} idRel \\le 𝓤 α$$$

Lean4

theorem refl_le_uniformity : 𝓟 idRel ≤ 𝓤 α :=
  (@UniformSpace.toCore α _).refl

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

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

Разделы

Аффилиация

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