Simple Digraph Suggestion

Stream: mathlib4

[Jafar Tanoukhi]

image.png
I opened a PR regarding formalizing Tournaments #28871. This person suggested adding Simple Digraphs as their own structure. Do you agree? I was told that in mathlib, it's best to keep structures to a minimum.

[Kyle Miller]

I think defining SimpleDigraph wouldn't help with your formalization. Using extends with structures doesn't serve as an inheritance mechanism.

For example, let's say someone has a Digraph and proves that it is loopless. Then, rather than being able to apply this tournament theory to it, they'd have to construct a SimpleDigraph, apply theorems to that, then somehow transfer the results back to the original Digraph.

I'd suggest sticking with Digraph here with this IsTournament predicate.

If there's some interesting structure on the type of all tournaments, you might consider it, to be able to define the relevant typeclass instances.