# Zulip Chat Archive

## Stream: graph theory

### Topic: cycles

#### Julian Berman (Oct 23 2020 at 23:09):

Hi! (new user to the stream and mostly in general). I want to exhibit a (finite) directed graph and prove it's a cycle, and then prove a thing or two about paths on it. Is this possibly a reasonable thing to attempt given any of the graph theory code that's been written? I see most of the code is likely on graph-theory-related branches of mathlib right?

#### Julian Berman (Oct 23 2020 at 23:12):

Oh, also -- I should mention by "exhibit" I mean "I have a function from X \to (set X)", so I want to get my graph by inducing it from that function.

#### Kyle Miller (Oct 24 2020 at 01:05):

We don't have directed graphs yet -- most energy has been put into simple graphs because of some basic complications to them that needed solving.

One thing about directed graphs without multiedges is that they're essentially just relations (indeed, `X -> set X`

is equivalent to `X -> X -> Prop`

), so you might get a lot of mileage out of what mathlib already has about those. For example, paths correspond the transitive closure of the relation.

#### Kyle Miller (Oct 24 2020 at 01:06):

Because of this, directed graphs will probably be with multiple edges, something like

```
structure dgraph_on (V : Type*) :=
(E : Type*)
(s : E → V)
(t : E → V)
```

#### Kyle Miller (Oct 24 2020 at 01:12):

https://leanprover-community.github.io/mathlib_docs/logic/relation.html#relation.refl_trans_gen

#### Julian Berman (Oct 24 2020 at 02:31):

Aha, thanks! That looks like a great breadcrumb, will have a look.

Last updated: May 08 2021 at 21:09 UTC