Прообраз функции в Изабель

Question

Я сделал это:

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

Нет ли встроенного определения, которое я мог бы использовать вместо этого? Как бы я нашел это?

Answer 1

f -` {a}

aka

vimage f {a}

Я нашел, ища теоремы с изображением имени в нем и надеясь найти правильную с символом:

find_theorems name:image

Я был повезло, что оно появилось в первых теоремах ... В общем, лучший подход - иметь представление о типе и использовать find_consts:

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