Theorems · Theorem · geometry

Projectivization.Subspace.span_eq_span_iff

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

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.

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