English
Let R be a (non-associative) semiring. The closure operation on subsets of R forms a Galois insertion with the inclusion of Subsemiring(R) into Set(R); equivalently, closure is the left adjoint to the inclusion map, and thus closure(s) is the smallest subsemiring of R containing s.
Русский
Пусть R — полусемиринг. Операция замыкания над подмножествами R образует Гало-инсерцию с включением Subsemiring(R) в Set(R); эквивалентно, замыкание является левым сопряжением к включению, следовательно, closure(s) наименьшее подполе полусемиринга R, содержащее s.
LaTeX
$$$\\forall X \\subseteq R:\\, X \\subseteq \\mathrm{closure}(X) \\ \\wedge\\ \\forall A\\,(A \\text{ подполе полусемиринга}\\ R \\wedge X \\subseteq A \\Rightarrow \\mathrm{closure}(X) \\subseteq A).$$$
Lean4
/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure R _) (↑)
where
choice s _ := closure s
gc _ _ := closure_le
le_l_u _ := subset_closure
choice_eq _ _ := rfl
