abs_signedInfDist_eq_dist_of_mem_affineSpan_insert

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]

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