gi — Mathlib · SciLib

English

There is a Galois insertion between affine spans and the set-coe map.

Русский

Существует Галуа-вставка между аффинной оболочкой и зачислением в множество.

LaTeX

$$$\\text{gi}: \\text{GaloisInsertion}(\\mathrm{affineSpan}(k), (\\cdot :\\, \\text{AffineSubspace}(k,P) \\to \\mathrm{Set}(P)))$$$

Lean4

/-- The Galois insertion formed by `affineSpan` and coercion back to a set. -/
protected def gi : GaloisInsertion (affineSpan k) ((↑) : AffineSubspace k P → Set P)
    where
  choice s _ := affineSpan k s
  gc s₁ _s₂ := ⟨fun h => Set.Subset.trans (subset_spanPoints k s₁) h, affineSpan_le_of_subset_coe⟩
  le_l_u _ := subset_spanPoints k _
  choice_eq _ _ := rfl

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