English
The direction of a Monge plane is the intersection of the orthogonal complement to the edge difference and the vector span of the simplex points.
Русский
Направление Monge-плоскости есть пересечение ортогонального дополнения к разности концов ребра и линейного пространства векоров вершин.
LaTeX
$$$$ (s.mongePlane(i_1,i_2)).direction = \min\{(\mathbb{R} \cdot (P_{i_1}-P_{i_2}))^{\perp}, \; \mathrm{vectorSpan}( \{P_0,\ldots,P_n\} )\}. $$$$
Lean4
/-- The Monge point is the only point in all the Monge planes from any
one vertex. -/
theorem eq_mongePoint_of_forall_mem_mongePlane {n : ℕ} {s : Simplex ℝ P (n + 2)} {i₁ : Fin (n + 3)} {p : P}
(h : ∀ i₂, i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂) : p = s.mongePoint :=
by
rw [← @vsub_eq_zero_iff_eq V]
have h' : ∀ i₂, i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ s.points i₁ -ᵥ s.points i₂)ᗮ ⊓ vectorSpan ℝ (Set.range s.points) :=
by
intro i₂ hne
rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]
exact h i₂ hne
have hi : p -ᵥ s.mongePoint ∈ ⨅ i₂ : { i // i₁ ≠ i }, (ℝ ∙ s.points i₁ -ᵥ s.points i₂)ᗮ :=
by
rw [Submodule.mem_iInf]
exact fun i => (Submodule.mem_inf.1 (h' i i.property)).1
rw [Submodule.iInf_orthogonal, ← Submodule.span_iUnion] at hi
have hu :
⋃ i : { i // i₁ ≠ i }, ({s.points i₁ -ᵥ s.points i} : Set V) =
(s.points i₁ -ᵥ ·) '' (s.points '' (Set.univ \ { i₁ })) :=
by
rw [Set.image_image]
ext x
simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton]
constructor
· rintro ⟨i, rfl⟩
use i, ⟨Set.mem_univ _, i.property.symm⟩
· rintro ⟨i, ⟨-, hi⟩, rfl⟩
use ⟨i, hi.symm⟩
rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi
have hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points) :=
by
let s₁ : Finset (Fin (n + 3)) := univ.erase i₁
obtain ⟨i₂, h₂⟩ := card_pos.1 (show 0 < #s₁ by simp [s₁, card_erase_of_mem])
have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm
exact (Submodule.mem_inf.1 (h' i₂ h₁₂)).2
exact Submodule.disjoint_def.1 (vectorSpan ℝ (Set.range s.points)).orthogonal_disjoint _ hv hi
