Mathlib v3 is deprecated. Go to Mathlib v4

Theorem local_homeomorph.extend_left_inv

Modification history

2023-03-09 17:31
src/geometry/manifold/smooth_manifold_with_corners.lean
feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680) …
Added local_homeomorph.extend_left_invView on Github →