Theorem OpenPartialHomeomorph.extend_target_eq_image_source

Modification history

2026-03-19 14:41
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
feat: smoothness on a set can be checked in extended charts (#36816) …
Added OpenPartialHomeomorph.extend_target_eq_image_sourceView on Github →