English
If a point p lies in all Monge planes determined by a fixed vertex i₁ and the remaining vertices, then p equals the Monge point of the simplex.
Русский
Если точка p лежит во всех Monge плоскостях, задаваемых фиксированной вершиной i₁ и другими вершинами, то p равно MongePoint симплекса.
LaTeX
$$$$ p = s.mongePoint \text{ if } \forall i_2, i_1 \neq i_2, p \in s.mongePlane(i_1,i_2). $$$$
Lean4
/-- A Monge plane of an (n+2)-simplex is the (n+1)-dimensional affine
subspace of the subspace spanned by the simplex that passes through
the centroid of an n-dimensional face and is orthogonal to the
opposite edge (in 2 dimensions, this is the same as an altitude).
This definition is only intended to be used when `i₁ ≠ i₂`. -/
def mongePlane {n : ℕ} (s : Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)) : AffineSubspace ℝ P :=
mk' (({ i₁, i₂ }ᶜ : Finset (Fin (n + 3))).centroid ℝ s.points) (ℝ ∙ s.points i₁ -ᵥ s.points i₂)ᗮ ⊓
affineSpan ℝ (Set.range s.points)
