English
The closure operation and the set-forgetful inclusion form a Galois insertion between Subgroups of G and subsets of G.
Русский
Операция замыкания и включение без изменения множества образуют Galois-поле между подгруппами группы G и подмножествами G.
LaTeX
$$$ \operatorname{closure} \dashv \iota : \mathrm{Subgroup}(G) \to \mathrm{Set}(G) $$$
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 G _) (↑)
where
choice s _ := closure s
gc s t := @closure_le _ _ t s
le_l_u _s := subset_closure
choice_eq _s _h := rfl
