Theorems · Theorem · geometry

AffineIndependent.inf_affineSpan_eq_affineSpan_inter

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ (s₁ s₂ : Set ι), affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂) = affineSpan k (p '' (s₁ ∩ s₂))

If a family is affinely independent, the infimum of the affine spans of points indexed by two subsets equals the affine span of points indexed by the intersection of those subsets, if the underlying ring is nontrivial.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Independent

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsorNontrivial