gi — Mathlib · SciLib

English

The closure operator on subsets of R forms a Galois insertion with the inclusion map into Set.

Русский

Оператор замыкания на подмножествaх R образует инсерцию Гало с включением в множество.

LaTeX

$$$\\mathrm{gi} : \\mathrm{GaloisInsertion}(\\mathrm{closure}, \\iota)$, с $\\mathrm{choice}(s)=\\mathrm{closure}(s)$, $\\mathrm{le\_l\_u}(s)=\\subseteq\\mathrm{closure}(s)$, и т.д.$$

Lean4

/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure R _) (↑)
    where
  choice s _ := closure s
  gc _s _t := closure_le
  le_l_u _s := subset_closure
  choice_eq _s _h := rfl

Похожие утверждения