Def FiberwiseLinear.partialHomeomorph

Modification history

2025-10-02 09:10

Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …

Deleted FiberwiseLinear.partialHomeomorph View on Github →

2024-01-08 13:15

Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

chore: last LocalHomeomorph -> PartialHomeomorph renames (#9238) …

Added FiberwiseLinear.partialHomeomorph View on Github →