span_eq_span_iff — Mathlib

English

Let S and T be subsets of the projective space ℙ_K(V). Then span S = span T if and only if S ⊆ span T and T ⊆ span S.

Русский

Пусть S и T — подмножества проективного пространства ℙ_K(V). Тогда порожденные мнества span S и span T равны тогда и только тогда, когда S ⊆ span T и T ⊆ span S.

LaTeX

$$$$ \\operatorname{span} S = \\operatorname{span} T \\iff S \\subseteq \\operatorname{span} T \\land T \\subseteq \\operatorname{span} S. $$$$

Lean4

/-- The spans of two sets of points in a projective space are equal if and only if each set of
points is contained in the span of the other set. -/
theorem span_eq_span_iff {S T : Set (ℙ K V)} : span S = span T ↔ S ⊆ span T ∧ T ⊆ span S :=
  ⟨fun h => ⟨h ▸ subset_span S, h.symm ▸ subset_span T⟩, fun h =>
    le_antisymm (span_le_subspace_iff.2 h.1) (span_le_subspace_iff.2 h.2)⟩

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