English
Let s be an affine simplex in a Euclidean setting. For distinct indices i ≠ j of the simplex vertices, the normalized inner product between the edge vectors joining each vertex to its altitude foot is strictly less than 1, i.e. |<s.points_i − s.altitudeFoot_i, s.points_j − s.altitudeFoot_j>| / (height_i height_j) < 1.
Русский
Пусть s — аффинный симплекс в евклидовом пространстве. Для различных индексов i ≠ j верно, что модуль скалярного произведения между векторами, ведущими от вершины к проекции на высоту, делённое на произведение высот, строго меньше 1: |<s.points_i − s.altitudeFoot_i, s.points_j − s.altitudeFoot_j>| / (height_i height_j) < 1.
LaTeX
$$$\\left| \\left< s.points_i -\\!\\cdot s.altitudeFoot i ,\, s.points_j -\\!\\cdot s.altitudeFoot j \\right> \\right| \\/ (s.height i \\cdot s.height j) < 1$$
Lean4
theorem abs_inner_vsub_altitudeFoot_div_lt_one {i j : Fin (n + 1)} (hij : i ≠ j) :
|⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)| < 1 :=
by
rw [abs_div, div_lt_one (by simp [height])]
nth_rw 2 [abs_eq_self.2]
· exact abs_inner_vsub_altitudeFoot_lt_mul _ hij
· simp only [height]
positivity
