subset_span — Mathlib

English

The span of a set of points is a Galois insertion between sets of points in the projective space and subspaces of the projective space.

Русский

Образ span множества точек образует вложение Гало между множествами точек проективного пространства и подпространствами пространства.

LaTeX

$$$\text{span} \ : \ \mathcal{P}(\mathbb{P}_K V) \to \mathrm{Subspace}(K V) \text{ and } \mathrm{SetLike.coe} \text{ form a Galois insertion}$$$

Lean4

/-- The span of a set of points contains the set of points. -/
theorem subset_span (S : Set (ℙ K V)) : S ⊆ span S := fun _x hx => spanCarrier.of _ hx

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