Isabelle 函数的原像

Question

我做了这个：

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

难道没有我可以使用的内置定义吗？我如何找到它？

Answer 1

f -` {a}

又名

vimage f {a}

我通过搜索名称为 image 的定理找到并希望找到带有符号的正确定理：

find_theorems name:image

我很幸运它出现在第一个定理中......一般来说，更好的方法是了解类型并使用 find_consts:

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

Preimage of a function in Isabelle