gi — Mathlib · SciLib

English

The span of a subspace is the subspace itself.

Русский

Спан подпространства является самим подпространством.

LaTeX

$$$\operatorname{span}(\uparrow W) = W$$$

Lean4

/-- The span of a set of points is a Galois insertion between sets of points of a projective space
and subspaces of the projective space. -/
def gi : GaloisInsertion (span : Set (ℙ K V) → Subspace K V) SetLike.coe
    where
  choice S _hS := span S
  gc A
    B :=
    ⟨fun h => le_trans (subset_span _) h, by
      intro h x hx
      induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'⟩
  le_l_u _ := subset_span _
  choice_eq _ _ := rfl

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