New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(geometry/manifold): redefine some instances #7124
Conversation
@gebner Could you please explain why implicit/explicit args matter here? Currently your commits look like black magic to me. |
The implicit/explicit args don't matter at all---for leanchecker. But apparently the elaborator now needs a little help with the new version of unique_diff_on. It can no longer figure out the second |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
bors d+
Thanks!
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…/mathlib into real-instance
There are no coercions from `euclidean_half_space n` or `euclidean_quadrant n` to `euclidean_space ℝ (fin n)`
bors merge |
* 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. Co-authored-by: @gebner Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Pull request successfully merged into master. Build succeeded: |
unique_diff_within_at
into astructure
.tangent_cone_at
,unique_diff_within_at
, andunique_diff_on
to asemimodule
that is atopological_space
.model_with_corners_euclidean_half_space
andmodel_with_corners_euclidean_quadrant
to reuse more generic lemmas, includingunique_diff_on.pi
andunique_diff_on.univ_pi
.model_with_corners.unique_diff'
usetarget
instead ofrange I
; usually it has better defeq.Co-authored-by: @gebner