gi — Mathlib · SciLib

English

The closure operator forms a Galois insertion with the coercion to sets; i.e., closure_L is left adjoint to the inclusion map from substructures to sets.

Русский

Оператор замыкания образует Галуа-инсерцию с вложением в множества; то есть closure_L — левый сопряжённый к включению подструктур в множества.

LaTeX

$$$$ \operatorname{closure}_L(s) \le S \iff s \subseteq (S :\, \text{Set} M). $$$$

Lean4

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

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