toColex

Mathlib.Order.Synonym

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

English

There is a canonical equivalence between α and Colex α given by the identity map.

Русский

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

LaTeX

$$$\alpha \simeq Colex\,\alpha$$$

Lean4

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

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

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

Разделы

Аффилиация

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