Commit 2023-12-03 19:31 d1931fcf

View on Github →

feat(ContDiff): define LocalHomeomorph.restrContDiff (#8605) Restrict the source and the target of a local homeomorphism to the sets where both f and f.symm are C^n.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

added theorem LocalHomeomorph.contDiffOn_restrContDiff_source

added theorem LocalHomeomorph.contDiffOn_restrContDiff_target

added def LocalHomeomorph.restrContDiff