search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 297 forks source link

feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types #19150

Open dtumad opened 1 year ago

dtumad commented 1 year ago

This PR gives lemmas for separating a sum over option α into the value at none plus a sum over α

Open in Gitpod

jcommelin commented 1 year ago

I think you want s/some/sum/ in the PR title, right?

dtumad commented 1 year ago

I also added versions for sum types when adding the has_sum versions of lemmas, since it's very similar to the case of option, just combining lemmas about sums over set.range and subtype.