finite): add a version of `set.finite.bUnion` (#19098)

Commit

2 years ago

feat(data/set/finite): add a version of `set.finite.bUnion` (#19098) Add `set.finite.Union` and `equiv.set_finite_iff`. From the sphere eversion project.

Author

urkud

Parents

a33d01f7

mathlib3 5bb9fffd - feat(data/set/finite): add a version of `set.finite.bUnion` (#19098)

mathlib3
5bb9fffd - feat(data/set/finite): add a version of `set.finite.bUnion` (#19098)