sign_eq_of_affineCombination_mem_affineSpan_single_lineMap

English

If an affine combination lies on the line joining two affine combinations in a lineMap construction, the two coefficients from the line are forced to have the same sign under the given constraints.

Русский

Если аффинное сочетание лежит на отрезке, образованном двумя другими аффинными сочетаниями через линейное отображение, то коэффициенты по двум точкам на линии имеют одинаковый знак при заданных ограничениях.

LaTeX

$$$\\text{AffineIndependent}(p) \\Rightarrow \\forall w,s,i_1,i_2,i_3\\in s,\\; i_1\\neq i_2, i_1\\neq i_3, i_2\\neq i_3, \\; \\forall c\\ (0

Lean4

/-- 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. -/
theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap {p : ι → P} (h : AffineIndependent k p) {w : ι → k}
    {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) {i₁ i₂ i₃ : ι} (h₁ : i₁ ∈ s) (h₂ : i₂ ∈ s) (h₃ : i₃ ∈ s) (h₁₂ : i₁ ≠ i₂)
    (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {c : k} (hc0 : 0 < c) (hc1 : c < 1)
    (hs : s.affineCombination k p w ∈ line[k, p i₁, AffineMap.lineMap (p i₂) (p i₃) c]) :
    SignType.sign (w i₂) = SignType.sign (w i₃) := by
  classical
  rw [← s.affineCombination_affineCombinationSingleWeights k p h₁, ←
    s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
  refine
    sign_eq_of_affineCombination_mem_affineSpan_pair h hw (s.sum_affineCombinationSingleWeights k h₁)
      (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
      (Finset.affineCombinationSingleWeights_apply_of_ne k h₁₂.symm)
      (Finset.affineCombinationSingleWeights_apply_of_ne k h₁₃.symm) ?_
  rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃, Finset.affineCombinationLineMapWeights_apply_right h₂₃]
  simp_all only [sub_pos, sign_pos]

Похожие утверждения