mathlib3 documentation

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 #

TODO #

def simple_graph.far_from_triangle_free {α : Type u_1} {𝕜 : Type u_2} [fintype α] [linear_ordered_field 𝕜] (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 α] [linear_ordered_field 𝕜] {G : simple_graph α} {ε : 𝕜} :

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 α] [linear_ordered_field 𝕜] {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 α] [linear_ordered_field 𝕜] {G H : simple_graph α} {ε : 𝕜} (hH : H G) (hG : G.far_from_triangle_free ε) (hcard : (G.edge_finset.card) - (H.edge_finset.card) < ε * (fintype.card α ^ 2)) :
theorem simple_graph.far_from_triangle_free.nonpos {α : Type u_1} {𝕜 : Type u_2} [fintype α] [linear_ordered_field 𝕜] {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 α] [linear_ordered_field 𝕜] {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 α] [linear_ordered_field 𝕜] {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 α] [linear_ordered_field 𝕜] {G : simple_graph α} {ε : 𝕜} [nonempty α] (hG : G.far_from_triangle_free ε) (hε : 0 < ε) :