compare_coe

Mathlib.Topology.UniformSpace.AbstractCompletion

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

English

Compare with coe: applying compare to a base point equals the base embedding of f a.

Русский

Применение сравнения к базовой точке дает базовое вложение f a.

LaTeX

$$$ \forall a:\alpha,\ pkg.compare pkg' (pkg.coe a) = pkg'.coe a $$$

Lean4

theorem compare_coe (a : α) : pkg.compare pkg' (pkg.coe a) = pkg'.coe a :=
  pkg.extend_coe pkg'.uniformContinuous_coe a

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

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

Разделы

Аффилиация

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