(Possibly) Infinite Trees (of Finite Degree)

Stream: graph theory

[Lukas Gerlach]

Hi!

I have a small formalization of possibly infinite trees of finite degree for one of my projects. The formalization is very much tailored towards that purpose but if you think that this might be useful for a more general audience, I would be up for contributing something like this to mathlib :)
(If you don't think that this is useful, then this is of course fine too.)

I've also given a talk about this at the #Leaning In! workshop recently.
#Leaning In! > Possibly Infinite Trees of Finite Degree
(Video available here)

I had already posted about this in the mathlib4 channel but unfortunately did not get a response. Maybe this is more suitable here anyway. This was the original message:
#mathlib4 > (Possibly) Infinite Trees (of Bounded Degree)

Let me know what you think about this!
Cheers :)