# Zulip Chat Archive

## Stream: graph theory

### Topic: Triangles

#### Yaël Dillies (Apr 29 2022 at 20:26):

Now that we have two PRs talking about triangles (#12988 and #13758), how should we name the files? I'm happy to go with `.triangle.free_far`

and `triangle.free`

.

#### Kyle Miller (Apr 29 2022 at 20:35):

I had been planning on putting the main content of #13758 into combinatorics/simple_graph/triangle/basic.lean once #12988 was merged, but I hadn't really thought about it.

Do you expect there to be a lot more general theory about triangles?

#### Mauricio Collares (Apr 29 2022 at 20:35):

Probably I shouldn't opine since I haven't contributed anything yet, but in both cases triangles are just a special case: Saying "G is \eps-far from being H-free" is an useful thing for any H, removal lemmas are useful for any fixed sugraph H and extremal numbers make sense for any H. To prepare for a future where all of these things are proved in more generality, theorems could be structured the other way around (`combinatorics.extremal.triangle`

, `combinatorics.removal.triangle`

and so on).

#### Mauricio Collares (Apr 29 2022 at 20:37):

If people want to do everything for triangles first (sounds like a good idea), stability and "supersaturation" for triangles would certainly be interesting.

#### Yaël Dillies (Apr 29 2022 at 20:37):

Yes, this is why I am against generalizing triangle-free-far to clique-free-far. For now, because we only have `combinatorics.simple_graph`

(which we could maybe shorten to `combinatorics.graph`

?) anyway, it doesn't make much sense to separate further but I agree.

#### Yaël Dillies (Apr 29 2022 at 20:39):

When I first opened #12988, it contained a definition of triangles and the finset of triangles. This really was basic. But those are now about cliques so it doesn't really make sense anymore.

#### Yaël Dillies (Apr 29 2022 at 20:39):

For now I suggest

`combinatorics.simple_graph.triangle.free`

`combinatorics.simple_graph.triangle.free_far`

`combinatorics.simple_graph.triangle.counting`

`combinatorics.simple_graph.triangle.removal`

Last updated: Aug 03 2023 at 10:10 UTC