English
Let α be a preorder. Define UpperBounds(S) = {a ∈ α | ∀ s ∈ S, s ≤ a} and LowerBounds(T) = {a ∈ α | ∀ t ∈ T, a ≤ t}. Then for all S,T ⊆ α, we have T ⊆ UpperBounds(S) if and only if S ⊆ LowerBounds(T). Consequently UpperBounds and LowerBounds form a Galois connection (with the first map taking values in the dual order).
Русский
Пусть α — частично упорядоченное множество. Определим верхние границы множества S как UpperBounds(S) = {a ∈ α | ∀ s ∈ S, s ≤ a}, и нижние границы множества T как LowerBounds(T) = {a ∈ α | ∀ t ∈ T, a ≤ t}. Тогда для любых S,T ⊆ α выполняется T ⊆ UpperBounds(S) тогда и только тогда S ⊆ LowerBounds(T). Следовательно пары UpperBounds и LowerBounds образуют связь Галуа (с учётом двойственного порядка в области UpperBounds).
LaTeX
$$$\\forall S,T \\subseteq \\alpha:\\ T \\subseteq \\operatorname{UpperBounds}(S) \\iff S \\subseteq \\operatorname{LowerBounds}(T).$$$
Lean4
theorem gc_upperBounds_lowerBounds :
GaloisConnection (OrderDual.toDual ∘ upperBounds : Set α → (Set α)ᵒᵈ)
(lowerBounds ∘ OrderDual.ofDual : (Set α)ᵒᵈ → Set α) :=
by simpa [GaloisConnection, subset_def, mem_upperBounds, mem_lowerBounds] using fun S T ↦ forall₂_swap
