l_u_le_trans

Mathlib.Order.GaloisConnection.Defs

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

English

For any b, the composition u ∘ l ∘ u equals u, i.e., u(l(u(b))) = u(b).

Русский

Для любого b выполняется u(l(u(b))) = u(b).

LaTeX

$$$\forall b:\; u(l(u(b))) = u(b)$$$

Lean4

theorem l_u_le_trans {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z :=
  (gc.monotone_l <| gc.le_u hxy).trans hyz

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

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

Разделы

Аффилиация

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