English
The equivalence of left and right commutativity statements: (∀ w, uXZ(uZW w) = uXY(uYW w)) ↔ (∀ x, lWZ(lZX x) = lWY(lYX x)).
Русский
Эквивалентность левой и правой форм коммутатии: (для всех w) ...
LaTeX
$$$$ (\forall w, uXZ(uZW w) = uXY(uYW w)) \iff (\forall x, lWZ(lZX x) = lWY(lYX x)). $$$$
Lean4
theorem l_comm_iff_u_comm {X : Type*} [PartialOrder 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) :
(∀ w : W, uXZ (uZW w) = uXY (uYW w)) ↔ ∀ x : X, lWZ (lZX x) = lWY (lYX x) :=
⟨hXY.l_comm_of_u_comm hZW hWY hXZ, hXY.u_comm_of_l_comm hZW hWY hXZ⟩
