mongePlane_comm — Mathlib

English

The Monge plane associated with vertices i₁ and i₂ equals that associated with i₂ and i₁.

Русский

Monge-плоскость, связанная вершинами i₁,i₂, равна Monge-плоскости, связанной вершинами i₂,i₁.

LaTeX

$$$$ s.mongePlane(i_1,i_2) = s.mongePlane(i_2,i_1). $$$$

Lean4

/-- The Monge plane associated with vertices `i₁` and `i₂` equals that
associated with `i₂` and `i₁`. -/
theorem mongePlane_comm {n : ℕ} (s : Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)) :
    s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁ := by
  simp_rw [mongePlane_def]
  congr 3
  · congr 1
    exact pair_comm _ _
  · ext
    simp_rw [Submodule.mem_span_singleton]
    constructor
    all_goals rintro ⟨r, rfl⟩; use -r; rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

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