mathlib
4d4b501e - chore(data/set/finite): rename some lemmas (#7241)

Commit
4 years ago
chore(data/set/finite): rename some lemmas (#7241) ### Revert some name changes from #5813 * `set.fintype_set_bUnion` → `set.fintype_bUnion`; * `set.fintype_set_bUnion'` → `set.fintype_bUnion'`; * `set.fintype_bUnion` → `set.fintype_bind`; * `set.fintype_bUnion'` → `set.fintype_bind'`; * `set.finite_bUnion` → `set.finite.bind`; ### Add a few lemmas * `set.finite_Union_Prop`; * add `set.seq` versions of lemmas/defs about `<*>` (they work for `α`, `β` in different universes).
Author
Parents
Loading