Theorem Finset.union_nonempty

Modification history

2024-12-02 13:47
Mathlib/Data/Finset/Lattice/Lemmas.lean
feat(Finset): `(s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty` (#19609) …
Added Finset.union_nonemptyView on Github →