Theorems · Theorem · geometry

Projectivization.Subspace.span_eq_of_le

∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
  S ⊆ ↑W → W ≤ Projectivization.Subspace.span S → Projectivization.Subspace.span S = W

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.

Defined in

Mathlib.LinearAlgebra.Projectivization.Subspace

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModule