ofColex

Mathlib.Order.Synonym

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

English

There is a canonical equivalence from Colex α to α given by the identity map.

Русский

Существует каноническое эквивалентное соответствие от Colex α к α, заданное идентичностью.

LaTeX

$$$\mathrm{ofColex} : Colex\,\alpha \simeq \alpha$$$

Lean4

/-- `ofColex` is the identity function from the `Colex` of a type. -/
@[match_pattern]
def ofColex : Colex α ≃ α :=
  Equiv.refl _

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

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

Разделы

Аффилиация

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