@[simp]

theorem Affine.Simplex.closedInterior_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Simplex k P n) : s.closedInterior.Nonempty