English
There is a natural Galois insertion between the power set of a space and the lattice of closed subsets, given by S ↦ cl(S) (the closure) and the inclusion map from closed sets to sets. In particular, for any subset S and closed C, cl(S) ⊆ C if and only if S ⊆ C.
Русский
Существует естественная Галуа-инсерция между множествами и замкнутыми подмножествами: отображение S ↦ cl(S) и инклюзия замкнутых множеств в множества. В частности, для любого подмножества S и замкнутого множества C выполняется cl(S) ⊆ C тогда и только тогда S ⊆ C.
LaTeX
$$$\forall S \subseteq \alpha, \forall C \subseteq \alpha\ (C\text{ закрыто}) : \quad \overline{S} \subseteq C \iff S \subseteq C.$$$
Lean4
/-- The Galois insertion between sets and closeds. -/
def gi : GaloisInsertion (@Closeds.closure α _) (↑)
where
choice s hs := ⟨s, closure_eq_iff_isClosed.1 <| hs.antisymm subset_closure⟩
gc := gc
le_l_u _ := subset_closure
choice_eq _s hs := SetLike.coe_injective <| subset_closure.antisymm hs
