# Triangles in graphs #

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 #

• SimpleGraph.FarFromTriangleFree: Predicate for a graph such that one must remove a lot of edges from it for it to become triangle-free. This is the crux of the Triangle Removal Lemma.

## TODO #

• Generalise FarFromTriangleFree to other graphs, to state and prove the Graph Removal Lemma.

A graph has edge-disjoint triangles if each edge belongs to at most one triangle.

Equations
• G.EdgeDisjointTriangles = (G.cliqueSet 3).Pairwise fun (x y : ) => (x y).Subsingleton
Instances For
def SimpleGraph.LocallyLinear {α : Type u_1} (G : ) :

A graph is locally linear if each edge belongs to exactly one triangle.

Equations
• G.LocallyLinear = (G.EdgeDisjointTriangles ∀ ⦃x y : α⦄, G.Adj x y∃ (s : ), G.IsNClique 3 s x s y s)
Instances For
theorem SimpleGraph.LocallyLinear.edgeDisjointTriangles {α : Type u_1} {G : } :
G.LocallyLinearG.EdgeDisjointTriangles
theorem SimpleGraph.EdgeDisjointTriangles.mono {α : Type u_1} {G : } {H : } (h : G H) (hH : H.EdgeDisjointTriangles) :
G.EdgeDisjointTriangles
@[simp]
theorem SimpleGraph.edgeDisjointTriangles_bot {α : Type u_1} :
.EdgeDisjointTriangles
@[simp]
theorem SimpleGraph.locallyLinear_bot {α : Type u_1} :
.LocallyLinear
theorem SimpleGraph.EdgeDisjointTriangles.map {α : Type u_1} {β : Type u_2} {G : } (f : α β) (hG : G.EdgeDisjointTriangles) :
().EdgeDisjointTriangles
theorem SimpleGraph.LocallyLinear.map {α : Type u_1} {β : Type u_2} {G : } (f : α β) (hG : G.LocallyLinear) :
().LocallyLinear
@[simp]
theorem SimpleGraph.locallyLinear_comap {α : Type u_1} {β : Type u_2} {G : } {e : α β} :
(SimpleGraph.comap (e) G).LocallyLinear G.LocallyLinear
theorem SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton {α : Type u_1} {G : } [] :
G.EdgeDisjointTriangles ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag{s : | s G.cliqueSet 3 e s.sym2}.Subsingleton
theorem SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton {α : Type u_1} {G : } [] :
G.EdgeDisjointTriangles∀ ⦃e : Sym2 α⦄, ¬e.IsDiag{s : | s G.cliqueSet 3 e s.sym2}.Subsingleton

Alias of the forward direction of SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton.

instance SimpleGraph.EdgeDisjointTriangles.instDecidable {α : Type u_1} {G : } [] [] [DecidableRel G.Adj] :
Decidable G.EdgeDisjointTriangles
Equations
• SimpleGraph.EdgeDisjointTriangles.instDecidable = decidable_of_iff (((G.cliqueFinset 3)).Pairwise fun (x y : ) => (x y).card 1)
instance SimpleGraph.LocallyLinear.instDecidable {α : Type u_1} {G : } [] [] [DecidableRel G.Adj] :
Decidable G.LocallyLinear
Equations
• SimpleGraph.LocallyLinear.instDecidable = And.decidable
theorem SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le {α : Type u_1} {G : } [] [] [DecidableRel G.Adj] (hG : G.EdgeDisjointTriangles) :
3 * (G.cliqueFinset 3).card G.edgeFinset.card
theorem SimpleGraph.LocallyLinear.card_edgeFinset {α : Type u_1} {G : } [] [] [DecidableRel G.Adj] (hG : G.LocallyLinear) :
G.edgeFinset.card = 3 * (G.cliqueFinset 3).card
def SimpleGraph.FarFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} (G : ) (ε : 𝕜) [] [DecidableRel G.Adj] :

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

Equations
• G.FarFromTriangleFree ε = G.DeleteFar (fun (H : ) => H.CliqueFree 3) (ε * ())
Instances For
theorem SimpleGraph.farFromTriangleFree_iff {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [DecidableRel G.Adj] :
G.FarFromTriangleFree ε ∀ ⦃H : ⦄ [inst : DecidableRel H.Adj], H GH.CliqueFree 3ε * () G.edgeFinset.card - H.edgeFinset.card
theorem SimpleGraph.farFromTriangleFree.le_card_sub_card {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [DecidableRel G.Adj] :
G.FarFromTriangleFree ε∀ ⦃H : ⦄ [inst : DecidableRel H.Adj], H GH.CliqueFree 3ε * () G.edgeFinset.card - H.edgeFinset.card

Alias of the forward direction of SimpleGraph.farFromTriangleFree_iff.

theorem SimpleGraph.FarFromTriangleFree.mono {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} {δ : 𝕜} [] [DecidableRel G.Adj] (hε : G.FarFromTriangleFree ε) (h : δ ε) :
G.FarFromTriangleFree δ
theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty' {α : Type u_1} {𝕜 : Type u_3} {G : } {H : } {ε : 𝕜} [] [] [DecidableRel G.Adj] [DecidableRel H.Adj] (hH : H G) (hG : G.FarFromTriangleFree ε) (hcard : G.edgeFinset.card - H.edgeFinset.card < ε * ()) :
(H.cliqueFinset 3).Nonempty
theorem SimpleGraph.farFromTriangleFree_of_disjoint_triangles {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [] [DecidableRel G.Adj] (tris : Finset ()) (htris : tris G.cliqueFinset 3) (pd : (tris).Pairwise fun (x y : ) => (x y).Subsingleton) (tris_big : ε * () tris.card) :
G.FarFromTriangleFree ε

If there are ε * (card α)^2 disjoint triangles, then the graph is ε-far from being triangle-free.

theorem SimpleGraph.EdgeDisjointTriangles.farFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [] [DecidableRel G.Adj] (hG : G.EdgeDisjointTriangles) (tris_big : ε * () (G.cliqueFinset 3).card) :
G.FarFromTriangleFree ε
theorem SimpleGraph.FarFromTriangleFree.lt_half {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [] [DecidableRel G.Adj] [] (hG : G.FarFromTriangleFree ε) :
ε < 2⁻¹
theorem SimpleGraph.FarFromTriangleFree.lt_one {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [] [DecidableRel G.Adj] [] (hG : G.FarFromTriangleFree ε) :
ε < 1
theorem SimpleGraph.FarFromTriangleFree.nonpos {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [DecidableRel G.Adj] [] (h₀ : G.FarFromTriangleFree ε) (h₁ : G.CliqueFree 3) :
ε 0
theorem SimpleGraph.CliqueFree.not_farFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [DecidableRel G.Adj] [] (hG : G.CliqueFree 3) (hε : 0 < ε) :
¬G.FarFromTriangleFree ε
theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [DecidableRel G.Adj] [] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) :
¬G.CliqueFree 3
theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty {α : Type u_1} {𝕜 : Type u_3} {G : } {ε : 𝕜} [] [] [DecidableRel G.Adj] [] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) :
(G.cliqueFinset 3).Nonempty