Theorem OpenPartialHomeomorph.contDiffOn_restrContDiff_target

Modification history

2026-04-17 18:09
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` (#34649) …
Modified OpenPartialHomeomorph.contDiffOn_restrContDiff_targetView on Github →
2025-10-02 09:10
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …
Added OpenPartialHomeomorph.contDiffOn_restrContDiff_targetView on Github →