mathlib3
ac8a1196 - chore(geometry/manifold): use `namespace`, rename `image` to `image_eq` (#6517)

Commit
4 years ago
chore(geometry/manifold): use `namespace`, rename `image` to `image_eq` (#6517) * use `namespace` command in `geometry/manifold/smooth_manifold_with_corners`; * rename `model_with_corners.image` to `model_with_corners.image_eq` to match `source_eq` etc; * replace `homeomorph.coe_eq_to_equiv` with `@[simp] lemma coe_to_equiv`; * add `continuous_linear_map.symm_image_image` and `continuous_linear_map.image_symm_image`; * add `unique_diff_on.image`, `continuous_linear_equiv.unique_diff_on_image_iff`.
Author
Parents
Loading