Theorems · Theorem · geometry

Affine.Simplex.inv_height_lt_sum_inv_height

∀ {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) [n.AtLeastTwo]
  (i : Fin (n + 1)), (s.height i)⁻¹ < ∑ j with j ≠ i, (s.height j)⁻¹

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 gives information about the location of the incenter (see excenterWeights_empty_lt_inv_two).

Defined in

Mathlib.Geometry.Euclidean.Incenter

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZeroNat.AtLeastTwo