# mathlib3documentation

combinatorics.simple_graph.triangle.basic

# Triangles in graphs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A triangle in a simple graph is a 3-clique, namely a set of three vertices that are pairwise adjacent.

This module defines and proves properties about triangles in simple graphs.

## Main declarations #

• simple_graph.far_from_triangle_free: Predicate for a graph to have enough triangles that, to remove all of them, one must one must remove a lot of edges. This is the crux of the Triangle Removal lemma.

## TODO #

• Generalise far_from_triangle_free to other graphs, to state and prove the Graph Removal Lemma.
• Find a better name for far_from_triangle_free. Added 4/26/2022. Remove this TODO if it gets old.
def simple_graph.far_from_triangle_free {α : Type u_1} {𝕜 : Type u_2} [fintype α] (G : simple_graph α) (ε : 𝕜) :
Prop

A simple graph is ε-triangle-free far if one must remove at least ε * (card α)^2 edges to make it triangle-free.

Equations
theorem simple_graph.far_from_triangle_free_iff {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} :
⦃H : ⦄ [_inst_3 : , H G H.clique_free 3 ε * ^ 2) (G.edge_finset.card) - (H.edge_finset.card)
theorem simple_graph.far_from_triangle_free.le_card_sub_card {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} :
⦃H : ⦄ [_inst_3 : , H G H.clique_free 3 ε * ^ 2) (G.edge_finset.card) - (H.edge_finset.card)

Alias of the forward direction of simple_graph.far_from_triangle_free_iff.

theorem simple_graph.far_from_triangle_free.mono {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε δ : 𝕜} (hε : G.far_from_triangle_free ε) (h : δ ε) :
theorem simple_graph.far_from_triangle_free.clique_finset_nonempty' {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G H : simple_graph α} {ε : 𝕜} (hH : H G) (hG : G.far_from_triangle_free ε) (hcard : (G.edge_finset.card) - (H.edge_finset.card) < ε * ^ 2)) :
theorem simple_graph.far_from_triangle_free.nonpos {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} [nonempty α] (h₀ : G.far_from_triangle_free ε) (h₁ : G.clique_free 3) :
ε 0
theorem simple_graph.clique_free.not_far_from_triangle_free {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} [nonempty α] (hG : G.clique_free 3) (hε : 0 < ε) :
theorem simple_graph.far_from_triangle_free.not_clique_free {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} [nonempty α] (hG : G.far_from_triangle_free ε) (hε : 0 < ε) :
theorem simple_graph.far_from_triangle_free.clique_finset_nonempty {α : Type u_1} {𝕜 : Type u_2} [fintype α] {G : simple_graph α} {ε : 𝕜} [nonempty α] (hG : G.far_from_triangle_free ε) (hε : 0 < ε) :