Zulip Chat Archive

Stream: Is there code for X?

Topic: Common graphs

Iván Renison (Oct 20 2023 at 20:12):

Is there code for common graphs like complete graphs ( $K_n$ ), cycle graphs ( $C_n$ ) and chain graphs?

Jireh Loreaux (Oct 20 2023 at 20:30):

docs#completeGraph

Jireh Loreaux (Oct 20 2023 at 20:36):

@loogle ⊢ SimpleGraph ?a

Jireh Loreaux (Oct 20 2023 at 20:37):

@loogle ⊢ SimpleGraph ?a

loogle (Oct 20 2023 at 20:37):

:search: completeGraph, emptyGraph, and 19 more

Kyle Miller (Oct 20 2023 at 20:37):

completeGraph is \top using the lattice structure

Kyle Miller (Oct 20 2023 at 20:38):

We've written cycle graphs and chain graphs before across a few projects, but they haven't yet been contributed to mathlib.

Jireh Loreaux (Oct 20 2023 at 20:40):

Kyle, did you define them on any fintype with a docs#CircularOrder using docs#SimpleGraph.hasse ? After realizing we didn't have it, that's what I was about to suggest.

Iván Renison (Oct 20 2023 at 20:41):

Thank you

Kyle Miller (Oct 20 2023 at 20:48):

I forgot about hasse. We have the chain graph as docs#SimpleGraph.pathGraph

Jireh Loreaux (Oct 20 2023 at 21:04):

Nevermind, my idea doesn't work anyway since it's not a Preorder. I should refrain from commenting about graph theory. :sweat_smile:

Yaël Dillies (Oct 20 2023 at 21:12):

Yeah, we have complete and chain graphs but cycle graphs are not in mathlib yet.

Last updated: Dec 20 2023 at 11:08 UTC