English
If α and β are Boolean algebras and l,u form a Galois connection, then the pair (compl ∘ u ∘ compl, compl ∘ l ∘ compl) forms a Galois connection. Intuitively, negation reverses order and preserves the adjoint structure.
Русский
Если между булеановскими алгебрами α и β образованы связи Галуа, то пара (¬ ∘ u ∘ ¬, ¬ ∘ l ∘ ¬) образует связь Галуа. По интуиции, отрицание меняет порядок, но сохраняет сопряженную структуру.
LaTeX
$$$$ \\text{GaloisConnection}(\\text{compl} \\circ u \\circ \\text{compl}, \\text{compl} \\circ l \\circ \\text{compl}). $$$$
Lean4
protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := fun a b ↦
by
dsimp
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
