toLex

Mathlib.Order.Synonym

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

English

There is a canonical correspondence between α and Lex α given by the identity map.

Русский

Существует каноническое эквивалентное соответствие между α и Lex α, заданное идентичной нотацией.

LaTeX

$$$\alpha \simeq Lex\,\alpha$$$

Lean4

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

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

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

Разделы

Аффилиация

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