Preimage of a function in Isabelle

Question

I made this:

abbreviation "preimage f y ≡ { x . f x = y }"

Isn't there a built-in definition I could be using instead? How would I find that?

Answer 1

f -` {a}

aka

vimage f {a}

I found by searching for theorems with the name image in it and hoping to find the right one with the symbol:

find_theorems name:image

I was lucky enough that it appeared in the first theorems... In general, a better approach is have an idea of the type and use find_consts:

find_consts "('a ⇒ 'b) ⇒ 'b set ⇒ 'a set"