Theorems · Theorem · convex and discrete geometry

Affine.Simplex.mem_interior_face_iff_sbtw

∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {n : ℕ}
  (s : Affine.Simplex R P n) {p : P} {i j : Fin (n + 1)} (h : i ≠ j),
  p ∈ (s.face ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)

A point lies in the interior of a 1-dimensional face of a simplex if and only if it lies strictly between its vertices.

Defined in

Mathlib.Analysis.Convex.Between

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingPartialOrderAddCommGroupModuleAddTorsorIsOrderedRingIsDomainModule.IsTorsionFree