[Merged by Bors] - feat: lemmas about partitions of unity #9635
Conversation
grunweg
added
awaiting-review
| simp only [finsupport, mem_support, Finite.mem_toFinset, mem_setOf_eq] | ||
|
|
||
| theorem sum_finsupport {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X} | ||
| (hx₀ : x₀ ∈ s := by trivial) : |
There was a problem hiding this comment.
I like this idea but we don't do it elsewhere in the library so I'd leave it out for now
| (hx₀ : x₀ ∈ s := by trivial) : | |
| (hx₀ : x₀ ∈ s) : |
and raise it in Zulip if you're interested enough
| /-- The support of a partition of unity at a point `x₀` | ||
| (i.e., the set of `i` such that `f i` doesn't vanish at `x₀`), as a `Finset`. -/ |
There was a problem hiding this comment.
We prefer whitespace after a section heading. Also this comment is a bit of a mouthful. Finally, every def / theorem in this section has the same arguments so let's use variables. Thus how about:
| /-- The support of a partition of unity at a point `x₀` | |
| (i.e., the set of `i` such that `f i` doesn't vanish at `x₀`), as a `Finset`. -/ | |
| variable {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) | |
| /-- The support of a partition of unity at a point `x₀` as a `Finset`. -/ |
and then I guess you'll need to add:
variable {x₀}
in between mem_finsupport and sum_finsupport.
There was a problem hiding this comment.
Changed. The explanation of "support" felt helpful to me, hence I had added it. I have demoted it to a parenthetical now.
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
Thanks for the review! |
- add `finsupport`: the support (the set of indices which functions are non-vanishing) at a point, as a `Finset` - every point has a neighbourhood on which only finitely many functions are non-vanishing From sphere-eversion; I'm just upstreaming results.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
finsupport: the support (the set of indices which functions are non-vanishing) at a point, as aFinsetFrom sphere-eversion; I'm just upstreaming results.