Theorems · Definition · geometry

AffineSubspace.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] →
            (s : AffineSubspace ℝ P) → [Nonempty ↥s] → [s.direction.HasOrthogonalProjection] → P → P →ᴬ[ℝ] ℝ

The signed distance between s and a point, in the direction of the reference point p. This is expected to be used when p does not lie in s (in the degenerate case where p lies in s, this yields 0) and when the point at which the distance is evaluated lies in the affine span of s and p (any component of the distance orthogonal to that span is disregarded).

Defined in

Mathlib.Geometry.Euclidean.SignedDist

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNonemptySubmodule.HasOrthogonalProjection