gi — Mathlib · SciLib

English

Span forms a Galois insertion with the set-coercion map from Submodule to Set.

Русский

Порождающееобразование образует инсерцию Гало с коэрцией: подпространство ⇢ множество.

LaTeX

$$$$\text{GI}(\operatorname{span}, \uparrow) \text{ is a Galois insertion }$$$$

Lean4

/-- `span` forms a Galois insertion with the coercion from submodule to set. -/
protected def gi : GaloisInsertion (@span R M _ _ _) (↑)
    where
  choice s _ := span R s
  gc _ _ := span_le
  le_l_u _ := subset_span
  choice_eq _ _ := rfl

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