orthogonalProjectionSpan — Mathlib

English

For any orthocentric system, there exists a real number r such that every triangle whose vertices lie in the system has circumradius r.

Русский

Для любой ортокцентрической системы существует число r так, что у каждого треугольника, вершины которого лежат в системе, радиус описанной окружности равен r.

LaTeX

$$$\\exists r \\in \\mathbb{R}, \\; \\forall t : \\text{Triangle } \\mathbb{R} P,\\; \\mathrm{range}(t.points) \\subseteq s \\rightarrow t.circumradius = r$$$

Lean4

/-- The orthogonal projection of a point `p` onto the hyperplane spanned by the simplex's points. -/
def orthogonalProjectionSpan {n : ℕ} (s : Simplex ℝ P n) : P →ᴬ[ℝ] affineSpan ℝ (Set.range s.points) :=
  orthogonalProjection (affineSpan ℝ (Set.range s.points))

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