Theorems · Theorem · geometry

AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan

∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  {s t : Finset V}, AffineIndependent k Subtype.val → affineSpan k ↑s < affineSpan k ↑t → s.card < t.card

If the affine span of an affine independent finset is strictly contained in the affine span of another finset, then its cardinality is strictly less than the cardinality of that finset.

Defined in

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModule