```
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`

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`

is there a particular reason `Ensemble Image`

isn't in standard library?

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: Jul 13 2024 at 04:02 UTC