Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] FYI: kernel :: ('a => 'b) => ('a * 'a) set

view this post on Zulip Email Gateway (Jul 03 2025 at 14:19):

From: Tobias Nipkow <nipkow@in.tum.de>
Dear Isabelle users,

I have added the kernel of a function (and its relationship to //) to Main:

definition kernel :: "('a => 'b) => ('a * 'a) set" where
"kernel f = {(x,y). f x = f y}"

It is a natural notion and I needed it on conjunction with quotients.

Best
Tobias

smime.p7s

Last updated: Jul 26 2025 at 12:43 UTC