Commit 2023-06-27 07:58 b04be394

View on Github →

feat: upgrade a boundaryless ModelWithCorners to a Homeomorph (#5508)

Estimated changes

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem ModelWithCorners.range_eq_univ

added def ModelWithCorners.toHomeomorph