[Merged by Bors] - feat(combinatorics/simple_graph/basic): edge deletion

[kmill]

Function to delete edges from a simple graph, and some associated lemmas.

Also defines sym2.to_rel as an inverse to sym2.from_rel.

---

[b-mehta]

Can you use this to give the has_compl instance rather than something ad-hoc there?

[kmill]

Can you use this to give the has_compl instance rather than something ad-hoc there?

I'm not sure what the right has_compl instance for subgraph would be. It seems there are options, but they're not involutions I think.

[b-mehta]

Can you use this to give the has_compl instance rather than something ad-hoc there?

I'm not sure what the right has_compl instance for subgraph would be. It seems there are options, but they're not involutions I think.

Ah sorry, I was thinking of has_sdiff instance on simple_graph, maybe it doesn't apply

[kmill]

@b-mehta It turns out everything is better in terms of just edge deletion on simple graphs themselves, so it's switched over to that.

I thought about using sdiff to implement this, but you still have the complication of defining a simple graph from an edge set (so need to make it loopless). It seemed to be more straightforward just defining it directly.

[b-mehta]

@b-mehta It turns out everything is better in terms of just edge deletion on simple graphs themselves, so it's switched over to that.

I thought about using sdiff to implement this, but you still have the complication of defining a simple graph from an edge set (so need to make it loopless). It seemed to be more straightforward just defining it directly.

Great! What about the opposite, ie using this to implement sdiff? That way you won't have the issue of making a simple graph from the edge set, since you'd be doing the reverse.

[kmill]

@b-mehta Ok, I added sym2.to_rel so that delete_edges has a similar definition to the has_sdiff instance, which uses adj := x.adj \ y.adj

[jcommelin]

lgtm

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests