Commit 2026-06-16 16:57 c5355507

feat: Add AffineEquiv.image_intrinsicInterior (#38275)

Summary

This PR generalizes the existing lemma AffineIsometry.image_intrinsicInterior to the setting of affine equivalences, yielding the corresponding result AffineEquiv.image_intrinsicInterior. Since affine equivalences are more general than affine isometries, the proof requires an additional finite-dimensionality assumption. The key extra input is that in finite-dimensional spaces, an affine equivalence induces a homeomorphism via AffineEquiv.toHomeomorphOfFiniteDimensional, so the assumptions are adjusted accordingly. Apart from these extra assumptions, the argument is essentially the same as for AffineIsometry.image_intrinsicInterior.

Collaboration

This PR was developed together with @imathwy.