orthogonalProjection_mem_subspace_eq_self

Mathlib.Geometry.Euclidean.Projection

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self

← MathLib Explorer

English

If p ∈ s, then the projection of p onto s is p itself.

Русский

Если p ∈ s, то проекция p на s равна p.

LaTeX

$$$ p \in s \Rightarrow \operatorname{orthogonalProjection} s p = p $$$

Lean4

@[simp]
theorem orthogonalProjection_mem_subspace_eq_self {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] (p : s) : orthogonalProjection s p = p :=
  by
  ext
  rw [orthogonalProjection_eq_self_iff]
  exact p.2

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

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

Разделы

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

Аффилиация

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