Theorems · Definition · geometry

Affine.Simplex.excenterWeightsUnnorm

{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 unnormalized weights of the vertices in an affine combination that gives an excenter with signs determined by the given set of indices (for the empty set, this is the incenter; for a singleton set, this is the excenter opposite a vertex). An excenter with those signs exists if and only if the sum of these weights is nonzero (so the normalized weights sum to 1).

Defined in

Mathlib.Geometry.Euclidean.Incenter

Cited by

36 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero