orthogonalProjection_circumcenter

English

The orthogonal projection of the circumcenter onto a face of a simplex is the circumcenter of that face.

Русский

Ортогональная проекция circumcenter на грань тетраэдра равна circumcenter этой грани.

LaTeX

$$$\mathrm{Proj}_{(s.face\,h)}(s.circumcenter)=(s.face\,h).circumcenter$$$

Lean4

/-- The orthogonal projection of the circumcenter onto a face is the
circumcenter of that face. -/
theorem orthogonalProjection_circumcenter {n : ℕ} (s : Simplex ℝ P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : ↑((s.face h).orthogonalProjectionSpan s.circumcenter) = (s.face h).circumcenter :=
  haveI hr : ∃ r, ∀ i, dist ((s.face h).points i) s.circumcenter = r :=
    by
    use s.circumradius
    simp [face_points]
  orthogonalProjection_eq_circumcenter_of_exists_dist_eq _ hr

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