u_top

Mathlib.Order.GaloisConnection.Defs

URI: https://scilib.ai/kg/mathlib#GaloisConnection.u_top

English

If β has a top, then u(⊤) = ⊤ under a Galois connection between α and β.

Русский

Если у β имеется верхняя граница, то при связи Галуа между α и β выполняется u(⊤) = ⊤.

LaTeX

$$$$ u(\top) = \top. $$$$

Lean4

theorem u_top [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤ :=
  gc.u_eq_top.2 le_top

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

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

Разделы

Аффилиация

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