comp_le_uniformity

Mathlib.Topology.UniformSpace.Defs

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

English

The composition of the uniformity is contained in the uniformity.

Русский

Композиця равномерности содержится в равномерности.

LaTeX

$$$((𝓤 α).lift' (\\lambda s. s \\circ s)) \\le 𝓤 α$$$

Lean4

theorem comp_le_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) ≤ 𝓤 α :=
  UniformSpace.comp

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

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

Разделы

Аффилиация

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