Theorems · Theorem · geometry

EuclideanGeometry.dist_orthogonalProjection_eq_infDist

∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  dist p ↑((EuclideanGeometry.orthogonalProjection s) p) = Metric.infDist p ↑s

The distance between a point and its orthogonal projection to a subspace equals the distance to that subspace as given by Metric.infDist. This is not a simp lemma since the simplest form depends on the context (if any calculations are to be done with the distance, the version with the orthogonal projection gives access to more lemmas about orthogonal projections that may be useful).

Defined in

Mathlib.Geometry.Euclidean.Projection

Cited by

5 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNonemptySubmodule.HasOrthogonalProjection