This isn't an equiv that I think we should have; it's a combination of Fintype.finsetEquivSet and Equiv.arrowCongr (and even then a specialisation of that!). Can you say more about what the results in this PR will be used for, since this looks to me like there should be a much more direct way of getting there.

My main goal is to show that #{v : List.Vector Bool n | v.val.count true = k} = n.choose k (for a proof that the binomial distribution is a convolution of Bernoulli's in a follow-up-PR). Since Mathlib already contains results on the cardinality of powersetCard k (univ : Fin n), my idea was to use equivalences to that type. The way it worked best was to show two equivalences, one to Fin n → Bool, and then to List.Vector Bool n.

I think I do not understand the link between Equiv_fnFinBool_finsetFin and the connection of Fintype.finsetEquivSet and Equiv.arrowCongr, since no Sets are involved here (only Finsets) and I have only one function-type and not two, which would be required for Equiv.arrowCongr.

The idea is that Finset (Fin n) is equivalent to Set (Fin n) by Fintype.finsetEquivSet, and Set (Fin n) is (equivalent to) Fin n -> Prop, which is equivalent to Fin n -> Bool.
For the result you mention, it's not clear to me that List.Vector is the right tool, I'd guess you want to stick with Fin n -> Bool or even Fin n -> Prop. Very little in mathlib actually uses List.Vector! @DavidLedvinka didn't you also do stuff linking the binomial distribution with Bernoullis?

I proved this result in this zulip thread https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Discrete.20Probability.20Proposal using characteristic functions. None of this (except some of the prereqs) was PRed to mathlib though.

Isn't there some decidability reason that this is still a useful definition? I think

[DecidableEq ι] : (ι → Bool) ≃ (Finset ι)

(or perhaps its reflection) is worth having.

I played around a bit with the series of equivalences (ι → Bool) ≃ (ι → Prop) ≃ Set ι ≃ (Finset ι) for some {ι : Type*} [DecidableEq ι] [Fintype ι] in comparison with the direct definition as given above. Unfolding all definitions shows that the series of equivalences equals the direct definition. I guess this means that the above definition shouldn't be there, right?

(ι → Bool) ≃ (ι → Prop) and Set ι ≃ (Finset ι) are not computable, right?

Yes, that is right. So, there is a difference in computability. Does this mean the definition should stay (or be placed somewhere else)?

_s aren't allowed in the names of defs, generally speaking.

Some other candidate names would be:

• arrowBoolEquivFinset
• Finset.equivArrowBool (after flipping the direction)
• Finset.univFilterEquiv (since in theory definitions should be named after what they do, not just their type)

Maybe @b-mehta has some suggestions too.

I went with arrowBoolEquivFinset, but am open to any other name...