Commit 2021-12-17 19:23 0b5f0a2d
View on Github →feat(data/finset/basic): add ite_subset_union, inter_subset_ite for finset (#10586)
Just a couple of lemmas to simplify expressions involving ite and union / inter on finsets, note that this is not related to set.ite.
From flt-regular.