English
The dual of a Galois connection is again a Galois connection: if gc is a GaloisConnection l u, then the dual with toDual ∘ u ∘ ofDual and toDual ∘ l ∘ ofDual forms a GaloisConnection.
Русский
Двойственный элемент связей Галуа снова образует связь Галуа: если gc — связь Галуа l u, то двойственный образ с toDual ∘ u ∘ ofDual и toDual ∘ l ∘ ofDual образует связь Галуа.
LaTeX
$$$\mathrm{GaloisConnection}(\mathrm{toDual} \circ u \circ \mathrm{ofDual}, \mathrm{toDual} \circ l \circ \mathrm{ofDual})$$$
Lean4
protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
GaloisConnection (OrderDual.toDual ∘ u ∘ OrderDual.ofDual) (OrderDual.toDual ∘ l ∘ OrderDual.ofDual) := fun a b =>
(gc b a).symm
