English
The operation closure on subsets of R forms a Galois insertion with the inclusion map to sets; i.e., closure is the left adjoint to the inclusion of NonUnitalSubring into Set.
Русский
Замыкание на подмножестве R образует вложение Гало—инсерцию с включением; то есть замыкание является левой подстановкой к включению NonUnitalSubring в Set.
LaTeX
$$$\\text{closure} \\dashv \\mathrm{SetLike.coe}$, i.e., closure is a Galois insertion with Set inclusion.$$
Lean4
/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure R _) SetLike.coe
where
choice s _ := closure s
gc _s _t := closure_le
le_l_u _s := subset_closure
choice_eq _s _h := rfl
