Theorems · Theorem · order theory

GaloisConnection.l_comm_iff_u_comm

∀ {X : Type u_2} [inst : PartialOrder X] {Y : Type u_3} [inst_1 : Preorder Y] {Z : Type u_4} [inst_2 : Preorder Z]
  {W : Type u_5} [inst_3 : PartialOrder W] {lYX : X → Y} {uXY : Y → X},
  GaloisConnection lYX uXY →
    ∀ {lWZ : Z → W} {uZW : W → Z},
      GaloisConnection lWZ uZW →
        ∀ {lWY : Y → W} {uYW : W → Y},
          GaloisConnection lWY uYW →
            ∀ {lZX : X → Z} {uXZ : Z → X},
              GaloisConnection lZX uXZ → ((∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x))

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

PartialOrderPreorderPreorderPartialOrder