Theorems · Theorem · geometry

Affine.Simplex.inv_height_eq_sum_mul_inv_dist

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (s.height i)⁻¹ =
    ∑ j with j ≠ i,
      -(inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)) *
        (s.height j)⁻¹

The inverse of the distance from one vertex to the opposite face, expressed as a sum of multiples of that quantity for the other vertices. The multipliers, expressed here in terms of inner products, are equal to the cosines of angles between faces (informally, the inverse distances are proportional to the volumes of the faces and this is equivalent to expressing the volume of a face as the sum of the signed volumes of projections of the other faces onto that face).

Defined in

Mathlib.Geometry.Euclidean.Incenter

Cited by

1 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero