coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection

English

For a 1-simplex, the projection onto the opposite face equals the opposite vertex point.

Русский

Для 1-симплекса проекция на противоположную грань равна противоположной вершине.

LaTeX

$$$$s.\text{faceOpposite } i).\operatorname{orthogonalProjectionSpan}(p) = s.points(i^{\mathrm{rev}}).$$$$

Lean4

theorem coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection {n : ℕ} {r₁ : ℝ} (s : Simplex ℝ P n) {p p₁o : P}
    (hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)) :
    ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑(s.orthogonalProjectionSpan p)) +ᵥ p₁o)) = p₁o :=
  congrArg ((↑) : _ → P) (orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ _ hp₁o)

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