Functions with explicit finite preimage

Stream: Is there code for X?

[Gian Cordana Sanjaya]

I want to see if this kind of data structure already exists in Mathlib. I'm sure it is, but I couldn't find it.

structure FiniteFiberFn (α β) where
  fn : α → β
  fiber : β → Finset α
  fiber_spec : ∀ a b, a ∈ fiber b ↔ fn a = b

[Yaël Dillies]

No, this doesn't exist