## Stream: Coq users

### Topic: Ensemble image

#### Quinn (Nov 07 2021 at 12:03):

``````Definition Image {A B} (X : Ensemble A) (f : A -> B) : Ensemble B
:=
fun y => exists x, X x /\ y = f x.

Theorem Image_sanity : Same_set _ (fun x => 10 <= x <= 20) (Image (fun x => 0 <= x <= 10) (fun x => x + 10)).
Proof.
unfold Same_set, Included, In, Image.
split; intros y Hy.
- exists (y - 10).
split; lia.
- destruct Hy as [x Hy].
lia.
Qed.
``````

in constructive math can I find an image while under uncertainty about the inverse? I was a little surprised and annoyed that I needed to know the inverse in order to do this proof about my image implementation, and it implies that i'd be limited in working with images for unknown `f`

#### Gaëtan Gilbert (Nov 07 2021 at 12:19):

from that theorem you can derive `forall y, 10 <= y <= 20 -> exists x, 0 <= x <= 10 /\ y = x + 10`
so you need the inverse up to `exists`

#### Quinn (Nov 07 2021 at 12:28):

is there a particular reason `Ensemble Image` isn't in standard library?

#### Karl Palmskog (Nov 07 2021 at 13:28):

the standard library is in general not very standard or complete. I'd recommend looking at alternative set libraries, such as those in Stdpp and finmap

Last updated: Feb 01 2023 at 13:03 UTC