Best place for convex combination and simplex interior

Stream: mathlib4

[Chu Zheng]

I would like to ask for advice on the best place in mathlib for the following three lemmas about convex combinations and the interior of a simplex.

/-- For a given simplex, a point strictly between a point in its closed interior
and a point in its interior lies in its interior. -/
lemma Simplex.mem_interior_of_lineMap_closedInterior_interior [IsStrictOrderedRing k] {n : ℕ}
    (s : Simplex k P n) {p q : P} (hp : p ∈ s.closedInterior) (hq : q ∈ s.interior) {t : k}
    (ht : t ∈ Set.Ioo 0 1) :
    AffineMap.lineMap p q t ∈ s.interior := by

/-- For a given simplex, a point strictly between a vertex and a point in the interior of
the opposite face lies in its interior. -/
lemma Simplex.mem_interior_of_lineMap_point_faceOpposite_interior [IsStrictOrderedRing k] {n : ℕ}
    [NeZero n] (s : Simplex k P n) {i : Fin (n + 1)} {q : P} (hq : q ∈ (s.faceOpposite i).interior)
    {t : k} (ht : t ∈ Set.Ioo 0 1) :
    AffineMap.lineMap (s.points i) q t ∈ s.interior := by

/-- For a given simplex, a point strictly between a point in the interior of one face and a point
in the interior of its complementary face lies in its interior. -/
lemma mem_interior_of_lineMap_face_interior_face_interior_compl [IsStrictOrderedRing k]
    {n mf mg : ℕ} (s : Simplex k P n) {fs gs : Finset (Fin (n + 1))} (hfs : #fs = mf + 1)
    (hgs : #gs = mg + 1) (hcompl : IsCompl fs gs) {p q : P} (hp : p ∈ (s.face hfs).interior)
    (hq : q ∈ (s.face hgs).interior) {t : k} (ht : t ∈ Set.Ioo 0 1) :
    AffineMap.lineMap p q t ∈ s.interior := by

These are straightforward facts about convex combinations preserving membership in the interior of a simplex.

Currently there is an Analysis/Convex/Between file containing many lemmas about sbtw.
Another candidate location is close to the Simplex.interior definition, e.g. LinearAlgebra/AffineSpace/Simplex/Basic. Which placement is preferred?

I did not formulate these lemmas using sbtw, because sbtw additionally requires the two endpoints to be distinct.

So my questions are:

• What is the best file for these lemmas?
• Should I change the statements to use sbtw rather than AffineMap.lineMap?
• Furthermore, do we need a separate file for convex results in affine spaces, especially those specific to Affine.Simplex?

Any guidance on the preferred organization would be appreciated. Thanks!