Commit 2022-01-04 13:36 a7aa2c87

feat(data/finset/sigma): A way to lift finset-valued functions to a sigma type (#10958) This defines finset.sigma_lift : (Π i, α i → β i → finset (γ i)) → Σ i, α i → Σ i, β i → finset (Σ i, γ i) as the function which returns the finset corresponding to the first coordinate of a b : Σ i, α i if they have the same, or the empty set else.