id

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderHom.id

English

The identity function is the identity element in the sense of OrderHom.

Русский

Идентичная функция служит единицей в рамках OrderHom.

LaTeX

$$$\\text{id}: \\alpha \\to_o \\alpha$; the underlying function is $\\mathrm{id}$ and it is monotone.$$

Lean4

/-- The identity function as bundled monotone function. -/
@[simps -fullyApplied]
def id : α →o α :=
  ⟨_root_.id, monotone_id⟩

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

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

Разделы

Аффилиация

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