(Possibly) Infinite Trees (of Bounded Degree)

Stream: mathlib4

[Lukas Gerlach]

Hi!

I have a small project where I work towards formalizing some database theory related definitions and results, which form the basis of some of my own (ongoing) research. Part of it is a definition of the "chase" on "disjunctive existential rules", which requires possibly infinite trees of bounded degree. At the moment, I have an (admittedly rather ad-hoc) formalization of such trees:
https://github.com/monsterkrampe/proof-library/blob/b533e058ba8875a72fca6951ffba520b6cec86c2/ProofLibrary/PossiblyInfiniteTree.lean
The idea is similar to using Stream' to represent infinite lists.

I am curious if the mathlib community would like to have something like this as part of the library. If this already exists in some form and I'm just not seeing it or if someone is already working on this, I would also be very interested to hear :)
(Of course feedback of any kind is also appreciated!)