# Zulip Chat Archive

## Stream: graph theory

### Topic: infinite union of graphs

#### Bhavik Mehta (Aug 21 2020 at 19:25):

Something interesting to think about: is there a nice way of doing this construction in Lean? For instance can you show that if G has no cycles of length four, then ext G is a friendship graph

#### Kyle Miller (Aug 21 2020 at 19:32):

What kind of union? A disjoint union, or a union of subgraphs within a particular universal graph?

#### Kyle Miller (Aug 21 2020 at 19:34):

Because, rather than defining `subgraph G`

to be a bounded lattice, it could be defined to be a complete lattice, so then an infinite union would be the `sup`

of an indexed family of subgraphs. (For example, `G`

could be a complete graph on some given vertex type.)

#### Kyle Miller (Aug 21 2020 at 19:37):

What's `ext G`

? (Is it something from Ramsey theory?)

#### Bhavik Mehta (Aug 21 2020 at 21:17):

Oh oops I meant to attach a picture - sorry

#### Bhavik Mehta (Aug 21 2020 at 21:18):

#### Bhavik Mehta (Aug 21 2020 at 21:19):

In particular in this setting when you're just given G, there's not an ambient graph in which all your subgraphs do form a lattice, so just taking `sup`

like you mention isn't immediate

#### Kyle Miller (Aug 22 2020 at 04:04):

Having colimits of graphs like that would be nice, though in this case you could define `ext G`

using a `sup`

construction on subgraphs of the complete graph on the set of binary trees with leaves being labeled by vertices of `G`

:

```
variables {α : Type u} [simple_graphs α]
inductive all_deriv_verts (G : α)
| incl (v : V G) : all_deriv_verts
| pair (v w : all_deriv_verts) : all_deriv_verts
def total (G : α) := complete_graph (all_deriv_verts G)
```

Here, `total G`

is the graph that's universal.

#### Bhavik Mehta (Aug 22 2020 at 13:16):

I suspect you want `pair`

to take a `sym2`

or finset of size 2 rather than an ordered pair, but yeah I can see that works

#### Kyle Miller (Aug 22 2020 at 16:56):

Oh, good catch

Last updated: May 08 2021 at 22:13 UTC