∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {r : ℝ} {p₀ p : P},
  p ∈ s.closedInterior →
    (∀ (i : Fin (n + 1)), p ≠ s.points i) → (∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r) → dist p p₀ < r