-
Notifications
You must be signed in to change notification settings - Fork 297
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] - feat(topology/support): add lemma locally_finite.exists_finset_nhd_mul_support_subset
#13006
Conversation
…ul_support_subseteq` When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point.
Do you ever need |
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Strictly speaking: no, I do not need this. However it is convenient and seems worth having. In my application I have a family of functions which are smooth on |
locally_finite.exists_finset_nhd_mul_support_subseteq
locally_finite.exists_finset_nhd_mul_support_subset
bors merge |
…ul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.
Build failed (retrying...): |
…ul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.
Pull request successfully merged into master. Build succeeded: |
locally_finite.exists_finset_nhd_mul_support_subset
locally_finite.exists_finset_nhd_mul_support_subset
…ul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.
…ul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.
…ul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.
The Mathlib PR leanprover-community/mathlib#13006 rendered these redundant. In fact the hope is to avoid this approach entirely by using `exists_cont_diff_of_convex` (or possibly a generalisation of it). However it's useful to start purging easy stuff from `to_mathlib`.
The Mathlib PR leanprover-community/mathlib#13006 rendered these redundant. In fact the hope is to avoid this approach entirely by using `exists_cont_diff_of_convex` (or possibly a generalisation of it). However it's useful to start purging easy stuff from `to_mathlib`.
When using a partition of unity to glue together a family of functions, this lemma allows
us to pass to a finite family in the neighbourhood of any point.
Formalized as part of the Sphere Eversion project.