Commit 2023-05-30 11:24 bc67f7e7

View on Github →

feat: add a version of Set.Finite.biUnion (#4469) forward-port leanprover-community/mathlib#19098

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

added theorem Equiv.set_finite_iff

added theorem Set.Finite.iUnion