Theorems · Definition · geometry

Affine.Simplex.signedInfDist

{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 → Fin (n + 1) → P →ᴬ[ℝ] ℝ

The signed distance between the face of s excluding point i of that simplex and a point, in the direction of the reference point i. This is expected to be used when the point at which the distance is evaluated lies in the affine span of the simplex (any component of the distance orthogonal to that span is disregarded). In the case of a triangle, these distances are trilinear coordinates; in a tetrahedron, they are quadriplanar coordinates.

Defined in

Mathlib.Geometry.Euclidean.SignedDist

Cited by

19 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero