Theorems · Theorem · geometry

sign_eq_of_affineCombination_mem_affineSpan_single_lineMap

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∀ {i₁ i₂ i₃ : ι},
          i₁ ∈ s →
            i₂ ∈ s →
              i₃ ∈ s →
                i₁ ≠ i₂ →
                  i₁ ≠ i₃ →
                    i₂ ≠ i₃ →
                      ∀ {c : k},
                        0 < c →
                          c < 1 →
                            (Finset.affineCombination k s p) w ∈ line[k, p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c] →
                              SignType.sign (w i₂) = SignType.sign (w i₃)

Given an affinely independent family of points, suppose that an affine combination lies in the span of one point of that family and a combination of another two points of that family given by lineMap with coefficient between 0 and 1. Then the coefficients of those two points in the combination lying in the span have the same sign.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Independent

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRingAddCommGroupModuleAddTorsor