compose — Mathlib

English

If l1,u1 and l2,u2 form Galois connections, then their composition forms a Galois connection: l2∘l1 and u1∘u2 are adjoint.

Русский

Если пары (l1,u1) и (l2,u2) образуют связи Галуа, то композиция l2∘l1 и u1∘u2 образуют сопряжение.

LaTeX

$$$$ \text{If } GC(l_1,u_1) \text{ and } GC(l_2,u_2), \ then GC(l_2\circ l_1,\ u_1\circ u_2). $$$$

Lean4

protected theorem compose [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β}
    (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) : GaloisConnection (l2 ∘ l1) (u1 ∘ u2) := fun _ _ ↦
  (gc2 _ _).trans (gc1 _ _)

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