## Stream: graph theory

### Topic: subgraphs

#### Jalex Stark (Aug 18 2020 at 01:17):

After chatting a bit with @Kyle Miller , we think that a main bottleneck is in getting a good definition of subgraph. Kyle has a good understanding of how submonoids work, (after the recent refactor led by uh kevin and scott?) and we'd like to get the behavior of subgraphs to be as similar as we can.

#### Jalex Stark (Aug 18 2020 at 01:19):

@Michael Hahn has some sorrys where the right hting to do is apply subgraph induction and then do some simple manipulations with subgraphs.

#### Jalex Stark (Aug 18 2020 at 01:22):

My attempt to specify the right lemmas for the induction principle is here https://github.com/apurvnakade/mc2020-projects/blob/master/src/michael/graph_induction.lean
and the rest of michael's graphs code is in the same folder in that repo.

#### Jalex Stark (Aug 18 2020 at 01:24):

A particularly frustrating thing is this sorry,

card_edges_erase (e : G.E) : (G.erase e).card_edges + 1 = G.card_edges := sorry


which I referenced earlier as being a thing that's annoying with card_edges.

Last updated: May 08 2021 at 22:13 UTC