English
If x, y, z are in weak betweenness along R, then the two edge vectors from x to y and from y to z point in the same ray.
Русский
Если x, y, z лежат в слабом между ними порядке, то вектор от x к y и вектор от y к z лежат на одном луче.
LaTeX
$$Wbtw(R,x,y,z) → SameRay(R, y - x, z - y)$$
Lean4
/-- A point lies in the interior of a 1-dimensional face of a simplex if and only if it lies
strictly between its vertices. -/
theorem mem_interior_face_iff_sbtw [Nontrivial R] [NoZeroSMulDivisors R V] {n : ℕ} (s : Simplex R P n) {p : P}
{i j : Fin (n + 1)} (h : i ≠ j) : p ∈ (s.face (Finset.card_pair h)).interior ↔ Sbtw R (s.points i) p (s.points j) :=
by
have h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (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 [sbtw_comm]
simp [max_eq_left hji.le, min_eq_right hji.le]
rw [h', mem_interior_iff_sbtw, face_points, face_points]
congr! 4
· convert Finset.orderEmbOfFin_zero _ _
· exact (Finset.min'_pair i j).symm
· omega
· convert Finset.orderEmbOfFin_last _ _
· exact (Finset.max'_pair i j).symm
· omega
