mem_closedInterior_face_iff_wbtw — Mathlib

English

The closed interior of a 1-dimensional face of a simplex equals the segment joining its two end vertices.

Русский

Замкнутая внутренняя часть 1-мерной грани симплекса равна отрезку, соединяющему её две вершины.

LaTeX

$${n : Nat} (s : Affine.Simplex R P n) {i j : Fin (n+1)} (h : i ≠ j) : (s.face (Finset.card_pair h)).closedInterior = affineSegment R (s.points i) (s.points j)$$

Lean4

/-- A point lies in the closed interior of a 1-dimensional face of a simplex if and only if it lies
weakly between its vertices. -/
theorem mem_closedInterior_face_iff_wbtw {n : ℕ} (s : Simplex R P n) {p : P} {i j : Fin (n + 1)} (h : i ≠ j) :
    p ∈ (s.face (Finset.card_pair h)).closedInterior ↔ Wbtw R (s.points i) p (s.points j) := by
  rw [s.closedInterior_face_eq_affineSegment h, Wbtw]

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