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 #

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 : Finset α) => (x y).Subsingleton
Instances For

    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 : Finset α), G.IsNClique 3 s x s y s)
    Instances For
      theorem SimpleGraph.LocallyLinear.edgeDisjointTriangles {α : Type u_1} {G : SimpleGraph α} :
      G.LocallyLinearG.EdgeDisjointTriangles
      theorem SimpleGraph.EdgeDisjointTriangles.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} (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 : SimpleGraph α} (f : α β) (hG : G.EdgeDisjointTriangles) :
      (SimpleGraph.map f G).EdgeDisjointTriangles
      theorem SimpleGraph.LocallyLinear.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α β) (hG : G.LocallyLinear) :
      (SimpleGraph.map f G).LocallyLinear
      @[simp]
      theorem SimpleGraph.locallyLinear_comap {α : Type u_1} {β : Type u_2} {G : SimpleGraph β} {e : α β} :
      (SimpleGraph.comap (⇑e) G).LocallyLinear G.LocallyLinear
      theorem SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton {α : Type u_1} {G : SimpleGraph α} :
      G.EdgeDisjointTriangles ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag{s : Finset α | s G.cliqueSet 3 e s.sym2}.Subsingleton
      theorem SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton {α : Type u_1} {G : SimpleGraph α} :
      G.EdgeDisjointTriangles∀ ⦃e : Sym2 α⦄, ¬e.IsDiag{s : Finset α | 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 : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] :
      Decidable G.EdgeDisjointTriangles
      Equations
      • SimpleGraph.EdgeDisjointTriangles.instDecidable = decidable_of_iff ((↑(G.cliqueFinset 3)).Pairwise fun (x y : Finset α) => (x y).card 1)
      instance SimpleGraph.LocallyLinear.instDecidable {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] :
      Decidable G.LocallyLinear
      Equations
      theorem SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] (hG : G.EdgeDisjointTriangles) :
      3 * (G.cliqueFinset 3).card G.edgeFinset.card
      theorem SimpleGraph.LocallyLinear.card_edgeFinset {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] (hG : G.LocallyLinear) :
      G.edgeFinset.card = 3 * (G.cliqueFinset 3).card
      def SimpleGraph.FarFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] (G : SimpleGraph α) (ε : 𝕜) [Fintype α] [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
      Instances For
        theorem SimpleGraph.farFromTriangleFree_iff {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] :
        G.FarFromTriangleFree ε ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H GH.CliqueFree 3ε * (Fintype.card α ^ 2) G.edgeFinset.card - H.edgeFinset.card
        theorem SimpleGraph.farFromTriangleFree.le_card_sub_card {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] :
        G.FarFromTriangleFree ε∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H GH.CliqueFree 3ε * (Fintype.card α ^ 2) 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} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} {δ : 𝕜} [Fintype α] [DecidableRel G.Adj] (hε : G.FarFromTriangleFree ε) (h : δ ε) :
        G.FarFromTriangleFree δ
        theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty' {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {H : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [DecidableRel H.Adj] [DecidableEq α] (hH : H G) (hG : G.FarFromTriangleFree ε) (hcard : G.edgeFinset.card - H.edgeFinset.card < ε * (Fintype.card α ^ 2)) :
        (H.cliqueFinset 3).Nonempty
        theorem SimpleGraph.farFromTriangleFree_of_disjoint_triangles {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [DecidableEq α] (tris : Finset (Finset α)) (htris : tris G.cliqueFinset 3) (pd : (↑tris).Pairwise fun (x y : Finset α) => (x y).Subsingleton) (tris_big : ε * (Fintype.card α ^ 2) 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} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [DecidableEq α] (hG : G.EdgeDisjointTriangles) (tris_big : ε * (Fintype.card α ^ 2) (G.cliqueFinset 3).card) :
        G.FarFromTriangleFree ε
        theorem SimpleGraph.FarFromTriangleFree.lt_half {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) :
        ε < 2⁻¹
        theorem SimpleGraph.FarFromTriangleFree.lt_one {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) :
        ε < 1
        theorem SimpleGraph.FarFromTriangleFree.nonpos {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (h₀ : G.FarFromTriangleFree ε) (h₁ : G.CliqueFree 3) :
        ε 0
        theorem SimpleGraph.CliqueFree.not_farFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.CliqueFree 3) (hε : 0 < ε) :
        ¬G.FarFromTriangleFree ε
        theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) :
        ¬G.CliqueFree 3
        theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] [DecidableEq α] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) :
        (G.cliqueFinset 3).Nonempty