l_top

Mathlib.Order.GaloisConnection.Defs

URI: https://scilib.ai/kg/mathlib#GaloisInsertion.l_top

← MathLib Explorer

English

The map u is strictly monotone: if a < b then u(a) < u(b).

Русский

Отображение u строго монотонно: если a < b, то u(a) < u(b).

LaTeX

$$$$ a < b \Rightarrow u(a) < u(b). $$$$

Lean4

theorem l_top [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β] (gi : GaloisInsertion l u) : l ⊤ = ⊤ :=
  top_unique <| (gi.le_l_u _).trans <| gi.gc.monotone_l le_top

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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