English
For a nondegenerate affine triangle t, there exists a betweenness relation holding for touchpoints with singleton sets.
Русский
Для невырожденного аффинного треугольника существует связь между касательными точками через одиночный набор.
LaTeX
$$$\exists\; Sbtw\,\text{(точки)}$$$
Lean4
theorem touchpoint_singleton_sbtw {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
Sbtw ℝ (t.touchpoint { i₁ } i₂) (t.points i₃) (t.points i₁) :=
by
rw [← Affine.Simplex.affineCombination_touchpointWeights]
have hw := t.sum_touchpointWeights { i₁ } i₂
rw [(by clear hw; decide +revert : (Finset.univ : Finset (Fin 3)) = { i₁, i₂, i₃ })] at hw
simp only [Nat.reduceAdd, Finset.mem_insert, h₁₂, Finset.mem_singleton, h₁₃, or_self, not_false_eq_true,
Finset.sum_insert, h₂₃, Simplex.touchpointWeights_eq_zero, Finset.sum_singleton, zero_add] at hw
have h :
t.touchpointWeights { i₁ } i₂ = Finset.affineCombinationLineMapWeights i₁ i₃ (t.touchpointWeights { i₁ } i₂ i₃) :=
by
ext i
have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert
rcases h with rfl | rfl | rfl
· rw [Finset.affineCombinationLineMapWeights_apply_left h₁₃]
simp [← hw]
· simp [h₁₂.symm, h₂₃]
· simp [h₁₃]
rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _),
sbtw_iff_right_ne_and_left_mem_image_Ioi]
simp [t.independent.injective.ne h₁₃, ← hw, t.touchpointWeights_singleton_neg h₁₂]
