graphs edge_finset

Stream: maths

[Shimon Cohen]

What I need to add to make it work?

import combinatorics.simple_graph.basic
import data.fintype.basic
import data.fintype.card
import data.fintype.powerset

open fintype

variables {V : Type*} [fintype V] [decidable_eq V]
#check {gm : simple_graph V // card (gm.edge_set) = 5}
#check {gm : simple_graph V // card (gm.edge_finset) = 5}

[Eric Wieser]

Does this work?

#check {gm : simple_graph V // ∃ decidable_rel gm.adj, by exactI card (gm.edge_finset) = 5}

[Eric Wieser]

(docs#simple_graph.edge_finset)

[Kyle Miller]

There's also avoiding decidability:

variables {V : Type*} -- optional: [fintype V]
#check {gm : simple_graph V // nat.card gm.edge_set = 5}

What to choose depends on what you're trying to do with this type though.

[Shimon Cohen]

Eric Wieser said:

Does this work?

#check {gm : simple_graph V // ∃ decidable_rel gm.adj, by exactI card (gm.edge_finset) = 5}

No ): error: "invalid binder, atomic identifier expected"

[Shimon Cohen]

Kyle Miller said:

There's also avoiding decidability:

variables {V : Type*} -- optional: [fintype V]
#check {gm : simple_graph V // nat.card gm.edge_set = 5}

What to choose depends on what you're trying to do with this type though.

where nat.card is defined?

[Kyle Miller]

docs#nat.card

[Shimon Cohen]

nice, I will try to use it with hope that inifinity will not hunt me later ;)