Commit 2020-11-22 22:06 f5b967ac
View on Github →feat(finset/basic): Add forall_mem_union (#5064) Part of [#4943](https://github.com/leanprover-community/mathlib/pull/4943), in order to prove theorems about antichains. Lemma and proof supplied by eric-wieser