Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-24 21:08 ead4731a

View on Github →

feat(geometry/manifold): model_with_corners is a closed_embedding (#6393)

Estimated changes

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem model_with_corners.closed_range

added theorem model_with_corners.image_mem_nhds_within

deleted theorem model_with_corners.left_inv'

added theorem model_with_corners.map_nhds_eq

added theorem model_with_corners.symm_comp_self

added theorem model_with_corners.symm_map_nhds_within_range

deleted theorem model_with_corners.target

added theorem model_with_corners.target_eq

Modified src/geometry/manifold/times_cont_mdiff.lean