Theorems · Theorem · order theory

GaloisConnection.u_comm_of_l_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 : Preorder 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 → (∀ (x : X), lWZ (lZX x) = lWY (lYX x)) → ∀ {w : W}, uXZ (uZW w) = uXY (uYW w)

Defined in: Mathlib.Order.GaloisConnection.Defs
Cited by: 2 results in Mathlib
Foundations: Depth 10 from the axioms · uses propext, Quot.sound
Assumes: PartialOrder Preorder Preorder Preorder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Preorderstatement and proof · cited by 7,952
PartialOrderstatement and proof · cited by 6,410
GaloisConnectionstatement and proof · cited by 253
GaloisConnection.composeproof · cited by 6
GaloisConnection.u_uniqueproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

Filter.smallSets_comap_eq_comap_imageproof · cited by 1
GaloisConnection.l_comm_iff_u_commproof · cited by 0