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 #

TODO #

def SimpleGraph.FarFromTriangleFree {α : Type u_1} {𝕜 : Type u_2} [Fintype α] [LinearOrderedField 𝕜] (G : SimpleGraph α) (ε : 𝕜) :

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

Instances For

    Alias of the forward direction of SimpleGraph.farFromTriangleFree_iff.

    theorem SimpleGraph.FarFromTriangleFree.mono {α : Type u_1} {𝕜 : Type u_2} [Fintype α] [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} {δ : 𝕜} (hε : SimpleGraph.FarFromTriangleFree G ε) (h : δ ε) :
    theorem SimpleGraph.FarFromTriangleFree.nonpos {α : Type u_1} {𝕜 : Type u_2} [Fintype α] [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Nonempty α] (h₀ : SimpleGraph.FarFromTriangleFree G ε) (h₁ : SimpleGraph.CliqueFree G 3) :
    ε 0
    theorem SimpleGraph.CliqueFree.not_farFromTriangleFree {α : Type u_1} {𝕜 : Type u_2} [Fintype α] [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Nonempty α] (hG : SimpleGraph.CliqueFree G 3) (hε : 0 < ε) :
    theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree {α : Type u_1} {𝕜 : Type u_2} [Fintype α] [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Nonempty α] (hG : SimpleGraph.FarFromTriangleFree G ε) (hε : 0 < ε) :