mathlib

a54db9a4 - feat(data/finset/basic): A finset that's a subset of a `directed` union is contained in one element (#13727)

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`