l_u_eq

Mathlib.Order.GaloisConnection.Defs

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

English

A GaloisInsertion ensures l(u(b)) = b for all b; equivalently u is a right inverse of l on β.

Русский

Связь Галуа гарантирует l(u(b)) = b; иными словами u является правым обратным к l на β.

LaTeX

$$$$ l(u(b)) = b $$$$

Lean4

theorem l_u_eq [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b :=
  (gi.gc.l_u_le _).antisymm (gi.le_l_u _)

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

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

Разделы

Аффилиация

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