feat(Geometry/Euclidean): Simplex.closedInterior is closed

[wwylele]

Intermediate lemma towards #34826. The immediate follow up is that the closed interior is measurable, but I'll leave it till the Measure folder appears under Geometry/Euclidean.

---

Not sure if this is the best place to put isClosed_closedInterior. It is a bit more general than other lemmas in the file (it needs minimal topological space assumptions instead of inner product space), but it still requires ℝ so I don't think it should be in the Topology folder.

[github-actions]

PR summary 99884c2730

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ closedInterior_eq_convexHull
+ isClosed_closedInterior

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Copilot]

Pull request overview

This pull request adds two theorems about the closed interior of simplices in Euclidean spaces, serving as an intermediate step towards calculating the volume of a simplex (PR #34826).

Changes:

• Proves that the closed interior of a simplex equals the convex hull of its vertices
• Establishes that the closed interior of a simplex is a closed set

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jsm28]

Does it really need ℝ, or would something weaker such as OrderClosedTopology suffice?

[jsm28]

I don't think either of the lemmas belongs in this file since they aren't specifically Euclidean.

[wwylele]

Right now the theorem that requires ℝ is Set.Finite.isClosed_convexHull, but I agree that this likely can be generalized. I'll look into it but this starts going into general topology that I am not good at. Please let me know if you have ideas for how to approach this.

[wwylele]

Did some preliminary research. The current dependency chain is like this

• Set.Finite.isClosed_convexHull (compact -> closed)
  • Set.Finite.isCompact_convexHull (compact -> compact image)
    • isCompact_stdSimplex (closed + bounded -> compact)
      • bounded_stdSimplex
      • isClosed_stdSimplex

All of these are currently stated for ℝ and potentially generalizable, with some caveats

• isClosed_stdSimplex can be generalized to OrderClosedTopology without problem
• bounded_stdSimplex needs some Bornology
• If we want to avoid compactness, isClosed_stdSimplex -> Set.Finite.isClosed_convexHull seems to be a good route, but the naive approach needs "closed -> closed image", i.e. an IsClosed linear map, which in turn requires the linear map to be injective. Unfortunately, the map from stdSimplex to convexHull is not necessarily injective.
• If we avoid convexHull all together, stdSimplex -> Simplex.closedInterior is injective because of the affine independence of Simplex, so the closeness is of Simplex.closedInterior can be proved this way.

So I guess with the new approach I'll need to set up direct mapping between stdSimplex and Simplex

[wwylele]

The map between stdSimplex and Simplex is obviously Finset.affineCombination and AffineBasis.coords, but lemma about continuity of these functions is also a bit lacking... for example, continuous_barycentric_coord is stated for normed space