English
If multiple Galois connections interact compatibly, then compositions on both sides commute: lWZ(lZX(x)) = lWY(lYX(x)).
Русский
Если несколько связей Галуа совместимы, композиции слева и справа согласованы: lWZ(lZX(x)) = lWY(lYX(x)).
LaTeX
$$$$ lWZ(lZX(x)) = lWY(lYX(x)) $$$$
Lean4
theorem l_comm_of_u_comm {X : Type*} [Preorder X] {Y : Type*} [Preorder Y] {Z : Type*} [Preorder Z] {W : Type*}
[PartialOrder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z}
(hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z}
{uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) (h : ∀ w, uXZ (uZW w) = uXY (uYW w)) {x : X} :
lWZ (lZX x) = lWY (lYX x) :=
(hXZ.compose hZW).l_unique (hXY.compose hWY) h
