compare

Mathlib.Topology.UniformSpace.AbstractCompletion

URI: https://scilib.ai/kg/mathlib#AbstractCompletion.compare

Lean4

/-- The comparison map between two completions of the same uniform space. -/
def compare : pkg.space → pkg'.space :=
  pkg.extend pkg'.coe

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

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

Разделы

Аффилиация

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