Commit 2025-07-10 04:21 02c6431f

View on Github →

feat: {Set,Finset}.mem_union_of_disjoint (#26946)

Estimated changes

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.mem_union_of_disjoint

Modified Mathlib/Data/Set/Disjoint.lean

added theorem Set.mem_union_of_disjoint