Is there a way to apply a function to a set in Coq using Ensemble?
That is, to define a function that takes a function f : A -> A
and a set S : Ensemble A
and returns an Ensemble A
such that for a , In A S a
(i.e. a
is an element of S
), the output set "contains" f a
.
If it is not (which I fear is the case), is there a different way to do this without having to resort to finite sets?