mathlib

9decec2b - feat(*): some simple lemmas about sets and finite sets (#1903)

feat(*): some simple lemmas about sets and finite sets (#1903) * feat(*): some simple lemmas about sets and finite sets * More lemmas, simplify proofs * Introduce `finsup.nonempty` and use it. * Update src/algebra/big_operators.lean Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * Revert "Update src/algebra/big_operators.lean" This reverts commit 17c89a808545203dc5a80a4f11df4f62e949df8d. It breaks compile if we rewrite right to left. * simp, to_additive * Add a missing docstring Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>