Documentation

Mathlib.Combinatorics.SimpleGraph.Clique

Graph cliques #

This file defines cliques in simple graphs. A clique is a set of vertices that are pairwise adjacent.

Main declarations #

TODO #

Cliques #

@[inline, reducible]
abbrev SimpleGraph.IsClique {α : Type u_1} (G : SimpleGraph α) (s : Set α) :

A clique in a graph is a set of vertices that are pairwise adjacent.

Instances For
    theorem SimpleGraph.isClique_iff {α : Type u_1} (G : SimpleGraph α) {s : Set α} :

    A clique is a set of vertices whose induced graph is complete.

    theorem SimpleGraph.IsClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {s : Set α} (h : G H) :
    theorem SimpleGraph.IsClique.subset {α : Type u_1} {G : SimpleGraph α} {s : Set α} {t : Set α} (h : t s) :

    Alias of the forward direction of SimpleGraph.isClique_bot_iff.

    n-cliques #

    structure SimpleGraph.IsNClique {α : Type u_1} (G : SimpleGraph α) (n : ) (s : Finset α) :

    An n-clique in a graph is a set of n vertices which are pairwise connected.

    Instances For
      theorem SimpleGraph.IsNClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : } {s : Finset α} (h : G H) :
      @[simp]
      theorem SimpleGraph.is3Clique_triple_iff {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] {a : α} {b : α} {c : α} :
      theorem SimpleGraph.is3Clique_iff {α : Type u_1} {G : SimpleGraph α} {s : Finset α} [DecidableEq α] :
      SimpleGraph.IsNClique G 3 s a b c, SimpleGraph.Adj G a b SimpleGraph.Adj G a c SimpleGraph.Adj G b c s = {a, b, c}

      Graphs without cliques #

      def SimpleGraph.CliqueFree {α : Type u_1} (G : SimpleGraph α) (n : ) :

      G.CliqueFree n means that G has no n-cliques.

      Instances For
        noncomputable def SimpleGraph.topEmbeddingOfNotCliqueFree {α : Type u_1} {G : SimpleGraph α} {n : } (h : ¬SimpleGraph.CliqueFree G n) :

        An embedding of a complete graph that witnesses the fact that the graph is not clique-free.

        Instances For
          theorem SimpleGraph.CliqueFree.mono {α : Type u_1} {G : SimpleGraph α} {m : } {n : } (h : m n) :
          theorem SimpleGraph.CliqueFree.anti {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : } (h : G H) :
          theorem SimpleGraph.cliqueFree_of_card_lt {α : Type u_1} {G : SimpleGraph α} {n : } [Fintype α] (hc : Fintype.card α < n) :

          See SimpleGraph.cliqueFree_of_chromaticNumber_lt for a tighter bound.

          A complete r-partite graph has no n-cliques for r < n.

          Set of cliques #

          def SimpleGraph.cliqueSet {α : Type u_1} (G : SimpleGraph α) (n : ) :
          Set (Finset α)

          The n-cliques in a graph as a set.

          Instances For

            Finset of cliques #

            def SimpleGraph.cliqueFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (n : ) :

            The n-cliques in a graph as a finset.

            Instances For