Commit 2021-04-22 10:34 8830a20f

refactor(geometry/manifold): redefine some instances (#7124)

• Turn unique_diff_within_at into a structure.
• Generalize tangent_cone_at, unique_diff_within_at, and unique_diff_on to a semimodule that is a topological_space.
• Redefine model_with_corners_euclidean_half_space and model_with_corners_euclidean_quadrant to reuse more generic lemmas, including unique_diff_on.pi and unique_diff_on.univ_pi.
• Make model_with_corners.unique_diff' use target instead of range I; usually it has better defeq.