u_comm_of_l_comm — Mathlib

English

Under the same compatibility assumptions, uXZ(uZW(w)) = uXY(uYW(w)).

Русский

При тех же предпосылках совместимости выполняется uXZ(uZW(w)) = uXY(uYW(w)).

LaTeX

$$$$ uXZ(uZW(w)) = uXY(uYW(w)) $$$$

Lean4

theorem u_comm_of_l_comm {X : Type*} [PartialOrder X] {Y : Type*} [Preorder Y] {Z : Type*} [Preorder Z] {W : Type*}
    [Preorder 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 : ∀ x, lWZ (lZX x) = lWY (lYX x)) {w : W} :
    uXZ (uZW w) = uXY (uYW w) :=
  (hXZ.compose hZW).u_unique (hXY.compose hWY) h

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