English
Suppose lines from two vertices of a triangle to interior points on the opposite side meet at p. Then p lies in the interior of the first (and by symmetry the other) segment from a vertex to its corresponding opposite-side point.
Русский
Пусть линии от двух вершин треугольника к точкам внутри противоположной стороны пересекаются в p. Тогда p лежит внутри первой (и симметрично другой) внутренности стороны от вершины к точке на противоположной стороне.
LaTeX
$$Sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair ...$$
Lean4
/-- Suppose lines from two vertices of a triangle to interior points of the opposite side meet at
`p`. Then `p` lies in the interior of the first (and by symmetry the other) segment from a
vertex to the point on the opposite side. -/
theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors R V] {t : Affine.Triangle R P}
{i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) {p₁ p₂ p : P} (h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃))
(h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)) (h₁' : p ∈ line[R, t.points i₁, p₁])
(h₂' : p ∈ line[R, t.points i₂, p₂]) : Sbtw R (t.points i₁) p p₁ :=
by
have h₁₃ : i₁ ≠ i₃ := by
rintro rfl
simp at h₂
have h₂₃ : i₂ ≠ i₃ := by
rintro rfl
simp at h₁
have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by omega
have hu : (Finset.univ : Finset (Fin 3)) = { i₁, i₂, i₃ } :=
by
clear h₁ h₂ h₁' h₂'
decide +revert
have hp : p ∈ affineSpan R (Set.range t.points) :=
by
have hle : line[R, t.points i₁, p₁] ≤ affineSpan R (Set.range t.points) :=
by
refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_
have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) :=
by
refine affineSpan_mono R ?_
simp [Set.insert_subset_iff]
rw [AffineSubspace.le_def'] at hle
exact hle _ h₁.wbtw.mem_affineSpan
rw [AffineSubspace.le_def'] at hle
exact hle _ h₁'
have h₁i := h₁.mem_image_Ioo
have h₂i := h₂.mem_image_Ioo
rw [Set.mem_image] at h₁i h₂i
rcases h₁i with ⟨r₁, ⟨hr₁0, hr₁1⟩, rfl⟩
rcases h₂i with ⟨r₂, ⟨hr₂0, hr₂1⟩, rfl⟩
rcases eq_affineCombination_of_mem_affineSpan_of_fintype hp with ⟨w, hw, rfl⟩
have h₁s :=
sign_eq_of_affineCombination_mem_affineSpan_single_lineMap t.independent hw (Finset.mem_univ _) (Finset.mem_univ _)
(Finset.mem_univ _) h₁₂ h₁₃ h₂₃ hr₁0 hr₁1 h₁'
have h₂s :=
sign_eq_of_affineCombination_mem_affineSpan_single_lineMap t.independent hw (Finset.mem_univ _) (Finset.mem_univ _)
(Finset.mem_univ _) h₁₂.symm h₂₃ h₁₃ hr₂0 hr₂1 h₂'
rw [← Finset.univ.affineCombination_affineCombinationSingleWeights R t.points (Finset.mem_univ i₁), ←
Finset.univ.affineCombination_affineCombinationLineMapWeights t.points (Finset.mem_univ _)
(Finset.mem_univ _)] at h₁' ⊢
refine
Sbtw.affineCombination_of_mem_affineSpan_pair t.independent hw
(Finset.univ.sum_affineCombinationSingleWeights R (Finset.mem_univ _))
(Finset.univ.sum_affineCombinationLineMapWeights (Finset.mem_univ _) (Finset.mem_univ _) _) h₁'
(Finset.mem_univ i₁) ?_
rw [Finset.affineCombinationSingleWeights_apply_self, Finset.affineCombinationLineMapWeights_apply_of_ne h₁₂ h₁₃,
sbtw_one_zero_iff]
have hs : ∀ i : Fin 3, SignType.sign (w i) = SignType.sign (w i₃) :=
by
intro i
rcases h3 i with (rfl | rfl | rfl)
· exact h₂s
· exact h₁s
· rfl
have hss : SignType.sign (∑ i, w i) = 1 := by simp [hw]
have hs' := sign_sum Finset.univ_nonempty (SignType.sign (w i₃)) fun i _ => hs i
rw [hs'] at hss
simp_rw [hss, sign_eq_one_iff] at hs
refine ⟨hs i₁, ?_⟩
rw [hu] at hw
rw [Finset.sum_insert, Finset.sum_insert, Finset.sum_singleton] at hw
· by_contra hle
rw [not_lt] at hle
exact (hle.trans_lt (lt_add_of_pos_right _ (Left.add_pos (hs i₂) (hs i₃)))).ne' hw
· simpa using h₂₃
· simpa [not_or] using ⟨h₁₂, h₁₃⟩
