Search code examples
coq

Coq: Is there a way to define "map" for Ensemble

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?

Solution

  • It's called Im and it's defined in the Image module.

    Require Import Ensembles Image.
About Im.
(* Im (X:Ensemble U) (f:U -> V) : Ensemble V *)