mongePoint_mem_mongePlane — Mathlib

English

The Monge point lies in every Monge plane associated to any pair of vertices.

Русский

MongePoint принадлежит каждой Monge-плоскости, связанной с любыми двумя вершинами.

LaTeX

$$$$ M \in s.mongePlane(i_1,i_2) \quad \text{for all } i_1,i_2. $$$$

Lean4

/-- The Monge point lies in the Monge planes. -/
theorem mongePoint_mem_mongePlane {n : ℕ} (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} :
    s.mongePoint ∈ s.mongePlane i₁ i₂ :=
  by
  rw [mongePlane_def, mem_inf_iff, ← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _), direction_mk',
    Submodule.mem_orthogonal']
  refine ⟨?_, s.mongePoint_mem_affineSpan⟩
  intro v hv
  rcases Submodule.mem_span_singleton.mp hv with ⟨r, rfl⟩
  rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]

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