order): Upper bound on the cardinality of `finset.bUnion` (#9797)

Commit

4 years ago

feat(algebra/big_operators/order): Upper bound on the cardinality of `finset.bUnion` (#9797) Also fix notation in all the additivized statements docstrings.

Author

YaelDillies

Parents

4df649cb

mathlib a7bc7174 - feat(algebra/big_operators/order): Upper bound on the cardinality of `finset.bUnion` (#9797)

mathlib
a7bc7174 - feat(algebra/big_operators/order): Upper bound on the cardinality of `finset.bUnion` (#9797)