Commit 2022-04-29 18:38 a54db9a4
View on Github →feat(data/finset/basic): A finset that's a subset of a directed union is contained in one element (#13727)
Proves directed.exists_mem_subset_of_finset_subset_bUnion
Renames finset.exists_mem_subset_of_subset_bUnion_of_directed_on to directed_on.exists_mem_subset_of_finset_subset_bUnion