coe_top

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Ici.coe_top

English

The top of Ici a maps to the top of α.

Русский

Верхний элемент Ici a отображается как верхний элемент α.

LaTeX

$$$$\\uparrow(\\top_{\\mathrm{Ici}(a)}) = \\top_{\\alpha}. $$$$

Lean4

@[simp, norm_cast]
protected theorem coe_top [Preorder α] [OrderTop α] (a : α) : ↑(⊤ : Ici a) = (⊤ : α) :=
  rfl

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

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

Разделы

Аффилиация

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