rfl
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ x ≤ r (r' z) ↔ x ≤ (r ∘ r') z
no goals