Commit 2024-12-02 13:47 4587215f

View on Github →

feat(Finset): (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty (#19609) From GrowthInGroups (LeanCamCombi)

Estimated changes

modified theorem Finset.union_eq_empty
added theorem Finset.union_nonempty