English
The closed interior of a 1-dimensional face of a simplex is the segment between its two endpoint vertices.
Русский
Замкнутая внутренняя часть 1-мерной грани симплекса — это отрезок между двумя вершинами этой грани.
LaTeX
$${n : Nat} (s : 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
/-- The closed interior of a 1-dimensional face of a simplex is a segment between its vertices. -/
theorem closedInterior_face_eq_affineSegment {n : ℕ} (s : 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) :=
by
have h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j)) :=
by
rcases h.lt_or_gt with hij | hji
· simp [min_eq_left hij.le, max_eq_right hij.le]
· nth_rw 2 [affineSegment_comm]
simp [max_eq_left hji.le, min_eq_right hji.le]
rw [h', (s.face (Finset.card_pair h)).closedInterior_eq_affineSegment, face_points, face_points]
congr 2
· convert Finset.orderEmbOfFin_zero _ _
· exact (Finset.min'_pair i j).symm
· omega
· convert Finset.orderEmbOfFin_last _ _
· exact (Finset.max'_pair i j).symm
· omega
