English
If p ∈ s and x ∈ affineSpan(insert p, s), then the absolute value of s.signedInfDist(p, x) equals the distance from x to the projection of x onto the opposite face of s.
Русский
Если p ∈ s и x ∈ афинальный охват (insert p) ∪ s, то |s.signedInfDist(p, x)| = dist(x, (faceOpposite i).orthogonalProjectionSpan(x)).
LaTeX
$$$|s.signedInfDist(p, x)| = \operatorname{dist}\bigl(x, (s.faceOpposite i).orthogonalProjectionSpan(x)\bigr)$$$
Lean4
theorem abs_signedInfDist_eq_dist_of_mem_affineSpan_insert {x : P} (h : x ∈ affineSpan ℝ (insert p s)) :
|s.signedInfDist p x| = dist x (orthogonalProjection s x) :=
by
rw [mem_affineSpan_insert_iff (orthogonalProjection s p).property] at h
rcases h with ⟨r, p₀, hp₀, rfl⟩
simp [hp₀, dist_eq_norm_vsub, orthogonalProjection_eq_self_iff.2 hp₀, orthogonalProjection_vsub_orthogonalProjection,
norm_smul, abs_mul]