orthogonalProjection_affineSpan_singleton

English

The projection of any point onto the affine span of a single point p1 is p1.

Русский

Проекция любой точки на аффинное пространство, порождаемое одним пунктом p1, равна p1.

LaTeX

$$$ \operatorname{orthogonalProjection}(\operatorname{affineSpan}(\mathbb{R}, \{p_1\})) p_2 = p_1 $$$

Lean4

@[simp]
theorem orthogonalProjection_affineSpan_singleton (p₁ p₂ : P) : orthogonalProjection (affineSpan ℝ { p₁ }) p₂ = p₁ :=
  by
  have h := SetLike.coe_mem (orthogonalProjection (affineSpan ℝ { p₁ }) p₂)
  rwa [mem_affineSpan_singleton] at h

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