Type issues (card for fintype and member of)

Stream: new members

[Christopher Schmidt]

Hello everyone,
I am working with (directed) graphs and V is supposed to be the set of vertices. Now I want to construct "A" such that A contains n vertices of V. I managed to do that V being a set of Naturals :

variables {V' : set ℕ}

structure vertex_subset_n {n : ℕ} {V' : set ℕ} :=
(verts : finset ℕ)
(sub : ∀ v ∈ verts, v ∈ V')
(card : verts.card = n)

But I would like to generalize it :

universe u
variables {V : Type u}

structure vertex_subset_n {n : ℕ} {V : Type u} :=
(verts : fintype V)
(sub : ∀ v ∈ verts, v ∈ V)
(card : verts.card = n)

How can I do this properly ? Obviously ∈ Vand verts.carddo not work. Any help is appreciated.

[Kevin Buzzard]

fintype V is the type of constructive proofs that V is a finite type, so verts : fintyoe V means "let verts be a proof that V is finite".

[Reid Barton]

You can just use verts : finset V, and get rid of sub

[Christopher Schmidt]

Thank you guys.