Synthesising Fintype for neighborSet

Stream: graph theory

[Chintada Srinivasa]

Using [Fintype V] and {G : SimpleGraph V}, how does one go about synthesising an instance of type class Fintype (G.neighborSet v) for any vertex v?

[Jihoon Hyun]

docs#SimpleGraph.neighborSet involves docs#SimpleGraph.Adj , so you probably need [DecidableRel G.Adj].

[Jakub Nowak]

@loogle |- Fintype (SimpleGraph.neighborSet _ _)

There's SimpleGraph.neighborSetFintype.

[loogle]

:search: SimpleGraph.neighborSetFintype, SimpleGraph.Subgraph.coeFiniteAt, and 1 more

[Chintada Srinivasa]

Worked out. Thanks!