mem_span — Mathlib

English

A point u in projective space lies in span S if and only if u lies in every subspace that contains S.

Русский

Точка u принадлежит span S тогда, когда она принадлежит любому подпространству, содержащему S.

LaTeX

$$$u \in \operatorname{span}(S) \iff \forall W\!:\, \mathrm{Subspace}(K,V),\; S \subseteq W \Rightarrow u \in W$$$

Lean4

/-- A point in a projective space is contained in the span of a set of points if and only if the
point is contained in all subspaces of the projective space which contain the set of points. -/
theorem mem_span {S : Set (ℙ K V)} (u : ℙ K V) : u ∈ span S ↔ ∀ W : Subspace K V, S ⊆ W → u ∈ W :=
  by
  simp_rw [← span_le_subspace_iff]
  exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩

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