Theorems · Theorem · geometry

AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Set ι},
      s.Nonempty →
        ∀ {w : ↑s → ι → k},
          (∀ (i : ↑s), ∑ j, w i j = 1) →
            ∀ {p' : P},
              (∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]) →
                ∃ w',
                  ∑ j, w' j = 1 ∧
                    (Finset.affineCombination k Finset.univ p) w' = p' ∧
                      ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j

A version of Ceva's theorem for a finite indexed affinely independent family of points: consider some lines, each through one of the points and an affine combination of the points, and suppose they concur at p'; then p' is an affine combination of the points with weights proportional to those in the respective affine combinations.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Ceva

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsorFintype