Zulip Chat Archive

Stream: graph theory

Topic: subgraphs


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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