u_unique

Mathlib.Order.GaloisConnection.Defs

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

← MathLib Explorer

English

There exists a b with a = u b if and only if a = u (l a).

Русский

Существует b такой, что a = u b тогда и только если a = u (l a).

LaTeX

$$$( \exists b:\beta, a = u b) \iff a = u (l a)$$$

Lean4

theorem u_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ a, l a = l' a) {b : β} : u b = u' b :=
  le_antisymm (gc'.le_u <| hl (u b) ▸ gc.l_u_le _) (gc.le_u <| (hl (u' b)).symm ▸ gc'.l_u_le _)

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

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

Разделы

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

Аффилиация

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