closure of Finset under a decreasing function

Stream: new members

[Malvin Gattinger]

Is there something like this in mathlib already?

def myClosure (h : DecidableEq α) (f : α → Finset α) (m : α → ℕ) (isDec : ∀ x, ∀ y ∈ f x, m y < m x):
  α → Finset α
  | S => {S} ∪ (f S) ∪ (f S).biUnion (myClosure h f m isDec) -- failed to prove termination
termination_by
  myClosure h f m isDec x => m x