Diagonal from a function

Stream: Is there code for X?

[Chase Fleming]

Hi, I see that there is the general definition of a diagonal in in set.prod, however, is there an existing definition for the set

def function_diagonal (f: α → β): set (α × α) := {p | f p.1 = f p.2}

[Yaël Dillies]

This is prod.map f f ⁻¹' diagonal β.

[Chase Fleming]

Thank you so much!