Theorems · Definition · geometry

Affine.Simplex.excenterWeights

{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 : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Fin (n + 1) → ℝ

The normalized weights of the vertices in an affine combination that gives an excenter with signs determined by the given set of indices. An excenter with those signs exists if and only if the sum of these weights is 1.

Defined in

Mathlib.Geometry.Euclidean.Incenter

Cited by

32 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero