feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584)
feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584)

Adds an `ext` lemma for simple graphs and an instance that there are finitely many if the vertex set is finite.



leanprover-community/mathlib,leanprover-community/mathlib