English
The closure operator on subsets of M is left adjoint to the inclusion of Subsemigroups into Set(M). Equivalently, for any subset s of M and any subsemigroup S, closure(s) ≤ S if and only if s ⊆ S.
Русский
Замыкание над множествами M является левым сопряжением включения подполугрупп в Set(M). Эквивалентно: closure(s) ≤ S тогда и только тогда, когда s ⊆ S.
LaTeX
$$$\\text{GI} :\\; \\mathrm{closure} \\dashv (\\text{SetLike.coe})\\, :\\; Subsemigroup M \\to\\ Set M$, и для любого $s\\subseteq M$, $S\\le \\mathrm{closure}(s) \\;\\Leftrightarrow\\; s \\subseteq S$$$
Lean4
/-- `closure` forms a Galois insertion with the coercion to set. -/
@[to_additive /-- `closure` forms a Galois insertion with the coercion to set. -/
]
protected def gi : GaloisInsertion (@closure M _) SetLike.coe :=
GaloisConnection.toGaloisInsertion (fun _ _ => closure_le) fun _ => subset_closure
