English
The upper closure operator forms a reversed Galois insertion with the coercion from upper sets to sets.
Русский
Оператор верхнего замыкания образует обращённую вставку Гало сказывание через включение верхних множеств в множества.
LaTeX
$${α : Type u} → [Preorder α] → GaloisInsertion (toDual ∘ upperClosure) ((↑) ∘ ofDual)$$
Lean4
/-- `upperClosure` forms a reversed Galois insertion with the coercion from upper sets to sets. -/
def giUpperClosureCoe : GaloisInsertion (toDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual)
where
choice s hs := toDual (⟨s, fun a _b hab ha => hs ⟨a, ha, hab⟩⟩ : UpperSet α)
gc := gc_upperClosure_coe
le_l_u _ := subset_upperClosure
choice_eq _s hs := ofDual.injective <| SetLike.coe_injective <| subset_upperClosure.antisymm hs
