feat(Geometry/Manifold): interior and boundary are preserved by (local) diffeomorphisms

[peabrainiac]

If f is a local diffeomorphism at x, f x is an interior point iff x is. We prove this and a bunch of corollaries, in particular that BoundarylessManifold is invariant under diffeomorphisms which we need for subsequent work.

---

• depends on: feat(Geometry/Manifold): the interior of a manifold is open #33189

[github-actions]

PR summary 6a39ceeb91

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary	2182	2217	+35 (+1.60%)

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime	3
Mathlib.Geometry.Manifold.WhitneyEmbedding	4
Mathlib.Geometry.Manifold.Riemannian.Basic	7
Mathlib.Geometry.Manifold.PoincareConjecture	9
Mathlib.Geometry.Manifold.Riemannian.PathELength	18
Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Topology.Compactification.OnePoint.Sphere	23
Mathlib.Geometry.Manifold.Instances.Icc	27
3 files Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary	35

---

Declarations diff

+ _root_.Diffeomorph.boundarylessManifold
+ _root_.Diffeomorph.boundarylessManifold_iff
+ _root_.Diffeomorph.image_boundary
+ _root_.Diffeomorph.image_interior
+ _root_.Diffeomorph.preimage_boundary
+ _root_.Diffeomorph.preimage_interior
+ _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv
+ _root_.IsLocalDiffeomorph.boundarylessManifold
+ _root_.IsLocalDiffeomorph.preimage_boundary
+ _root_.IsLocalDiffeomorph.preimage_interior
+ _root_.IsLocalDiffeomorphAt.isBoundaryPoint_iff
+ _root_.IsLocalDiffeomorphAt.isInteriorPoint_iff
+ _root_.IsLocalDiffeomorphOn.preimage_boundary_inter
+ _root_.IsLocalDiffeomorphOn.preimage_interior_inter
+ _root_.MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv
+ contDiffOn_extCoordChange
+ contDiffOn_extCoordChange_symm
+ extCoordChange
+ extCoordChange_symm
+ isBoundaryPoint_iff_not_isInteriorPoint
+ isBoundaryPoint_iff_of_mem_atlas
+ isClosed_boundary
+ isInteriorPoint_iff_of_mem_atlas
+ isInvertible_fderivWithin_extCoordChange
+ isOpen_interior
+ mem_frontier_iff_notMem_interior
+ mem_interior_iff_notMem_frontier
+ uniqueDiffOn_extCoordChange_source
+ uniqueDiffOn_extCoordChange_target
+ writtenInExtChartAt_mapsTo

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 script/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Geometry/Manifold): the interior of a manifold is open #33189
  By Dependent Issues (🤖). Happy coding!