feat(combinatorics/simple_graph/subgraph): single-vertex and single-edge subgraphs

[kmill]

Constructors for single-vertex and single-edge subgraphs along with some associated properties. Also includes dot notation improvements for simple_graph.subgraph.adj.

Co-authored-by: Joanna Choules [email protected]

---

[kmill]

@jchoules I collected some results I had about single-vertex and single-edge subgraphs along with some of your lemmas from #16382. I'm not sure about names -- you had vertex_singleton and edge_singleton, and here (because that's how they were in my branch) they're singleton_subgraph and subgraph_of_adj.

[jchoules]

I chose my names largely in reference to the specific roles those subgraphs played in the proof I was writing: your names seem more apt for general use.

[b-mehta]

LGTM!

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

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