Why is equiv.perm.support defined as a finset

Stream: general

[Mantas Baksys]

I found that equiv.perm.support is defined as a finset. Is there any particular reason for this? If not, should it be lifted so set instead? I found this painful for deducing the rearrangement inequality in a linear order (see #10861), as then you cannot really afford the fintype instance on the index set for the most common applications , so you can no longer use equiv.perm.support. Thanks!

[Yakov Pechersky]

I had a branch on which I generalized perm.support to work on types that are not necessarily fintype. However, membership in the support simp-normalizes to "f x != x" anyway. So you can express things in that way.

[Mantas Baksys]

Yakov Pechersky said:

I had a branch on which I generalized perm.support to work on types that are not necessarily fintype. However, membership in the support simp-normalizes to "f x != x" anyway. So you can express things in that way.

Yeah, that is clearly the alternative. I'll go with it then, just thought that I'd rather try to use equiv.perm.support because it exists