signedInfDist

Mathlib.Geometry.Euclidean.SignedDist

URI: https://scilib.ai/kg/mathlib#AffineSubspace.signedInfDist

Lean4

/-- 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). -/
noncomputable def signedInfDist : P →ᴬ[ℝ] ℝ :=
  signedDist (p -ᵥ orthogonalProjection s p) (Classical.ofNonempty : s)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru