English
A Galois connection is a pair of order-preserving maps l: α → β and u: β → α such that l a ≤ b iff a ≤ u b for all a ∈ α, b ∈ β.
Русский
Связь Галуа – пары отображений, сохраняющих порядок: l: α → β и u: β → α такие, что l a ≤ b эквивалентно a ≤ u b для всех a ∈ α, b ∈ β.
LaTeX
$$$\mathrm{GaloisConnection}\;l\;u \;\iff\; \forall a\in\alpha, b\in\beta: \; l a \le b \;\iff\; a \le u b$$$
Lean4
/-- A Galois connection is a pair of functions `l` and `u` satisfying
`l a ≤ b ↔ a ≤ u b`. They are special cases of adjoint functors in category theory,
but do not depend on the category theory library in mathlib. -/
def GaloisConnection [Preorder α] [Preorder β] (l : α → β) (u : β → α) :=
∀ a b, l a ≤ b ↔ a ≤ u b
