Pullback well-foundedness

Stream: Is there code for X?

[Yaël Dillies]

Do we have this? Maybe it requires f injective.

variables {α β : Type*}

/-- Pullback well-foundedness. -/
protected lemma well_founded.inv_image {r : β → β → Prop} (f : α → β) (h : well_founded r) :
  well_founded (inv_image r f) := sorry

[Chris Bailey]

Is this docs#inv_image.wf

[Yaël Dillies]

Yep, thanks!