Removing a point from a simplex

Stream: Is there code for X?

[Eric Wieser]

Do we have this somewhere?

import Mathlib.Geometry.Euclidean.MongePoint

open scoped BigOperators RealInnerProductSpace

namespace Affine.Simplex

variable {V : Type*} {P : Type*}
variables [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]

/-- Get the face of `s` that doesn't include `i` -/
def faceWithout {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) :
    Affine.Simplex ℝ P n where
  points := s.points ∘ Fin.succAbove i
  Independent := s.Independent.comp_embedding <| (Fin.succAboveEmb i).toEmbedding

[Eric Wieser]

(relatedly: #8419 fixes the misnamed Independent field)

[Johan Commelin]

cc @Yaël Dillies , maybe?

[Antoine Chambert-Loir]

Or @Sophie Morel ?

[Yaël Dillies]

Nope, don't have it. That's the kind of stuff you'd need for simplicial homology but I was more directly interested in Sperner's theorem.

[Joël Riou]

It seems it is related to Affine.Simplex.face, but with different definitional properties.

[Sophie Morel]

Antoine Chambert-Loir said:

Or Sophie Morel ?

Haven't done it, sorry. I've only worked with abstract simplicial complexes so far.