span_eq_of_le — Mathlib

English

If S ⊆ W and W ≤ span S, then span S = W.

Русский

Если S ⊆ W и W ≤ span S, тогда span S = W.

LaTeX

$$$S \subseteq W \land W \le \operatorname{span}(S) \Rightarrow \operatorname{span}(S) = W$$$

Lean4

/-- If a set of points in projective space is contained in a subspace, and that subspace is
contained in the span of the set of points, then the span of the set of points is equal to
the subspace. -/
theorem span_eq_of_le {S : Set (ℙ K V)} {W : Subspace K V} (hS : S ⊆ W) (hW : W ≤ span S) : span S = W :=
  le_antisymm (span_le_subspace_iff.mpr hS) hW

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