English
If there are at least two vertices, then for every i, 1/h_i is strictly less than the sum of 1/h_j over all j ≠ i.
Русский
При двух и более вершинах для каждого i верно: 1/h_i < сумма по j ≠ i 1/h_j.
LaTeX
$$$ (h_i)^{-1} < \sum_{j \neq i} (h_j)^{-1} $$$
Lean4
/-- The inverse of the distance from one vertex to the opposite face is less than the sum of that
quantity for the other vertices. This implies the existence of the excenter opposite that vertex;
it also implies that the image of the incenter under a homothety with scale factor 2 about a
vertex lies outside the simplex. -/
theorem inv_height_lt_sum_inv_height [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
(s.height i)⁻¹ < ∑ j ∈ {k | k ≠ i}, (s.height j)⁻¹ :=
by
rw [inv_height_eq_sum_mul_inv_dist]
refine Finset.sum_lt_sum_of_nonempty ?_ ?_
· rw [Finset.filter_ne', ← Finset.card_ne_zero]
simp only [Finset.mem_univ, Finset.card_erase_of_mem, Finset.card_univ, Fintype.card_fin, add_tsub_cancel_right]
exact NeZero.ne _
· rintro j hj
refine mul_lt_of_lt_one_left ?_ ?_
· simp [height_pos]
· rw [neg_lt]
exact neg_one_lt_inner_vsub_altitudeFoot_div _ _ _
