# Documentation

Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

# 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.
def SimpleGraph.FarFromTriangleFree {α : Type u_1} {𝕜 : Type u_2} [] (G : ) (ε : 𝕜) :

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

Instances For
theorem SimpleGraph.farFromTriangleFree_iff {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} :
∀ ⦃H : ⦄, H Gε * ↑()
theorem SimpleGraph.farFromTriangleFree.le_card_sub_card {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} :
∀ ⦃H : ⦄, H Gε * ↑()

Alias of the forward direction of SimpleGraph.farFromTriangleFree_iff.

theorem SimpleGraph.FarFromTriangleFree.mono {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} {δ : 𝕜} (hε : ) (h : δ ε) :
theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty' {α : Type u_1} {𝕜 : Type u_2} [] {G : } {H : } {ε : 𝕜} (hH : H G) (hG : ) (hcard : < ε * ↑()) :
theorem SimpleGraph.FarFromTriangleFree.nonpos {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} [] (h₀ : ) (h₁ : ) :
ε 0
theorem SimpleGraph.CliqueFree.not_farFromTriangleFree {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} [] (hG : ) (hε : 0 < ε) :
theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} [] (hG : ) (hε : 0 < ε) :
theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty {α : Type u_1} {𝕜 : Type u_2} [] {G : } {ε : 𝕜} [] (hG : ) (hε : 0 < ε) :