direction_mongePlane — Mathlib

English

If for a fixed i₁ a point p lies in all Monge planes s.mongePlane(i₁,i₂) for every i₂ ≠ i₁, then p equals the Monge point.

Русский

Если при фиксированной вершине i₁ точка p лежит во всех Monge-плоскостях s.mongePlane(i₁,i₂) для всех i₂ ≠ i₁, тогда p = MongePoint.

LaTeX

$$$$ \forall i_2, i_1 \neq i_2, p \in s.mongePlane(i_1,i_2) \Rightarrow p = s.mongePoint. $$$$

Lean4

/-- The direction of a Monge plane. -/
theorem direction_mongePlane {n : ℕ} (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} :
    (s.mongePlane i₁ i₂).direction = (ℝ ∙ s.points i₁ -ᵥ s.points i₂)ᗮ ⊓ vectorSpan ℝ (Set.range s.points) := by
  rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk', direction_affineSpan]

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