neg_one_lt_inner_vsub_altitudeFoot_div

English

For the same simplex s and indices i ≠ j, the ratio of the inner product to the product of heights satisfies a strict lower bound: -1 < ⟨s.points_i − s.altitudeFoot_i, s.points_j − s.altitudeFoot_j⟩ / (height_i height_j).

Русский

Для того же симплекса s и для i ≠ j выполняется неравенство: -1 < ⟨s.points_i − s.altitudeFoot_i, s.points_j − s.altitudeFoot_j⟩ / (height_i height_j).

LaTeX

$$$-1 < \\dfrac{\\langle s.points_i -\\!\\cdot s.altitudeFoot i , s.points_j -\\!\\cdot s.altitudeFoot j \\rangle}{s.height i \\cdot s.height j}$$$

Lean4

theorem neg_one_lt_inner_vsub_altitudeFoot_div (s : Simplex ℝ P n) (i j : Fin (n + 1)) :
    -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j) :=
  by
  rw [neg_lt, neg_div', div_lt_one (by simp [height]), neg_lt]
  exact neg_mul_lt_inner_vsub_altitudeFoot _ _ _

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