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 #

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

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

Equations
  • G.IsClique s = s.Pairwise G.Adj
Instances For
    theorem SimpleGraph.isClique_iff {α : Type u_1} (G : SimpleGraph α) {s : Set α} :
    G.IsClique s s.Pairwise G.Adj
    theorem SimpleGraph.isClique_iff_induce_eq {α : Type u_1} (G : SimpleGraph α) {s : Set α} :
    G.IsClique s SimpleGraph.induce s G =

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

    Equations
    • G.instDecidableIsCliqueToSetOfDecidableEqOfDecidableRelAdj = decidable_of_iff' ((↑s).Pairwise G.Adj)
    theorem SimpleGraph.isClique_empty {α : Type u_1} {G : SimpleGraph α} :
    G.IsClique
    theorem SimpleGraph.isClique_singleton {α : Type u_1} {G : SimpleGraph α} (a : α) :
    G.IsClique {a}
    theorem SimpleGraph.IsClique.of_subsingleton {α : Type u_1} {s : Set α} {G : SimpleGraph α} (hs : s.Subsingleton) :
    G.IsClique s
    theorem SimpleGraph.isClique_pair {α : Type u_1} {G : SimpleGraph α} {a : α} {b : α} :
    G.IsClique {a, b} a bG.Adj a b
    @[simp]
    theorem SimpleGraph.isClique_insert {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} :
    G.IsClique (insert a s) G.IsClique s bs, a bG.Adj a b
    theorem SimpleGraph.isClique_insert_of_not_mem {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} (ha : as) :
    G.IsClique (insert a s) G.IsClique s bs, G.Adj a b
    theorem SimpleGraph.IsClique.insert {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} (hs : G.IsClique s) (h : bs, a bG.Adj a b) :
    G.IsClique (insert a s)
    theorem SimpleGraph.IsClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {s : Set α} (h : G H) :
    G.IsClique sH.IsClique s
    theorem SimpleGraph.IsClique.subset {α : Type u_1} {G : SimpleGraph α} {s : Set α} {t : Set α} (h : t s) :
    G.IsClique sG.IsClique t
    @[simp]
    theorem SimpleGraph.isClique_bot_iff {α : Type u_1} {s : Set α} :
    .IsClique s s.Subsingleton
    theorem SimpleGraph.IsClique.subsingleton {α : Type u_1} {s : Set α} :
    .IsClique ss.Subsingleton

    Alias of the forward direction of SimpleGraph.isClique_bot_iff.

    theorem SimpleGraph.IsClique.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} (h : G.IsClique s) {f : α β} :
    (SimpleGraph.map f G).IsClique (f '' s)
    theorem SimpleGraph.isClique_map_iff_of_nontrivial {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α β} {t : Set β} (ht : t.Nontrivial) :
    (SimpleGraph.map f G).IsClique t ∃ (s : Set α), G.IsClique s f '' s = t
    theorem SimpleGraph.isClique_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α β} {t : Set β} :
    (SimpleGraph.map f G).IsClique t t.Subsingleton ∃ (s : Set α), G.IsClique s f '' s = t
    @[simp]
    theorem SimpleGraph.isClique_map_image_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} {f : α β} :
    (SimpleGraph.map f G).IsClique (f '' s) G.IsClique s
    theorem SimpleGraph.isClique_map_finset_iff_of_nontrivial {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α β} {t : Finset β} (ht : t.Nontrivial) :
    (SimpleGraph.map f G).IsClique t ∃ (s : Finset α), G.IsClique s Finset.map f s = t
    theorem SimpleGraph.isClique_map_finset_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α β} {t : Finset β} :
    (SimpleGraph.map f G).IsClique t t.card 1 ∃ (s : Finset α), G.IsClique s Finset.map f s = t
    theorem SimpleGraph.IsClique.finsetMap {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α β} {s : Finset α} (h : G.IsClique s) :
    (SimpleGraph.map f G).IsClique (Finset.map f s)

    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.

    • clique : G.IsClique s
    • card_eq : s.card = n
    Instances For
      theorem SimpleGraph.IsNClique.clique {α : Type u_1} {G : SimpleGraph α} {n : } {s : Finset α} (self : G.IsNClique n s) :
      G.IsClique s
      theorem SimpleGraph.IsNClique.card_eq {α : Type u_1} {G : SimpleGraph α} {n : } {s : Finset α} (self : G.IsNClique n s) :
      s.card = n
      theorem SimpleGraph.isNClique_iff {α : Type u_1} (G : SimpleGraph α) {n : } {s : Finset α} :
      G.IsNClique n s G.IsClique s s.card = n
      instance SimpleGraph.instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] [DecidableRel G.Adj] {n : } {s : Finset α} :
      Decidable (G.IsNClique n s)
      Equations
      • G.instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj = decidable_of_iff' (G.IsClique s s.card = n)
      @[simp]
      theorem SimpleGraph.isNClique_empty {α : Type u_1} {G : SimpleGraph α} {n : } :
      G.IsNClique n n = 0
      @[simp]
      theorem SimpleGraph.isNClique_singleton {α : Type u_1} {G : SimpleGraph α} {n : } {a : α} :
      G.IsNClique n {a} n = 1
      theorem SimpleGraph.IsNClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : } {s : Finset α} (h : G H) :
      G.IsNClique n sH.IsNClique n s
      theorem SimpleGraph.IsNClique.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : } {s : Finset α} (h : G.IsNClique n s) {f : α β} :
      (SimpleGraph.map f G).IsNClique n (Finset.map f s)
      theorem SimpleGraph.isNClique_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : } (hn : 1 < n) {t : Finset β} {f : α β} :
      (SimpleGraph.map f G).IsNClique n t ∃ (s : Finset α), G.IsNClique n s Finset.map f s = t
      @[simp]
      theorem SimpleGraph.isNClique_bot_iff {α : Type u_1} {n : } {s : Finset α} :
      .IsNClique n s n 1 s.card = n
      @[simp]
      theorem SimpleGraph.isNClique_zero {α : Type u_1} {G : SimpleGraph α} {s : Finset α} :
      G.IsNClique 0 s s =
      @[simp]
      theorem SimpleGraph.isNClique_one {α : Type u_1} {G : SimpleGraph α} {s : Finset α} :
      G.IsNClique 1 s ∃ (a : α), s = {a}
      theorem SimpleGraph.IsNClique.insert {α : Type u_1} {G : SimpleGraph α} {n : } {s : Finset α} {a : α} [DecidableEq α] (hs : G.IsNClique n s) (h : bs, G.Adj a b) :
      G.IsNClique (n + 1) (insert a s)
      theorem SimpleGraph.is3Clique_triple_iff {α : Type u_1} {G : SimpleGraph α} {a : α} {b : α} {c : α} [DecidableEq α] :
      G.IsNClique 3 {a, b, c} G.Adj a b G.Adj a c G.Adj b c
      theorem SimpleGraph.is3Clique_iff {α : Type u_1} {G : SimpleGraph α} {s : Finset α} [DecidableEq α] :
      G.IsNClique 3 s ∃ (a : α) (b : α) (c : α), G.Adj a b G.Adj a c G.Adj b c s = {a, b, c}
      theorem SimpleGraph.is3Clique_iff_exists_cycle_length_three {α : Type u_1} {G : SimpleGraph α} :
      (∃ (s : Finset α), G.IsNClique 3 s) ∃ (u : α) (w : G.Walk u u), w.IsCycle w.length = 3

      Graphs without cliques #

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

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

      Equations
      • G.CliqueFree n = ∀ (t : Finset α), ¬G.IsNClique n t
      Instances For
        theorem SimpleGraph.IsNClique.not_cliqueFree {α : Type u_1} {G : SimpleGraph α} {n : } {s : Finset α} (hG : G.IsNClique n s) :
        ¬G.CliqueFree n
        theorem SimpleGraph.not_cliqueFree_of_top_embedding {α : Type u_1} {G : SimpleGraph α} {n : } (f : ↪g G) :
        ¬G.CliqueFree n
        noncomputable def SimpleGraph.topEmbeddingOfNotCliqueFree {α : Type u_1} {G : SimpleGraph α} {n : } (h : ¬G.CliqueFree n) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem SimpleGraph.not_cliqueFree_iff {α : Type u_1} {G : SimpleGraph α} (n : ) :
          ¬G.CliqueFree n Nonempty ( ↪g G)
          theorem SimpleGraph.cliqueFree_iff {α : Type u_1} {G : SimpleGraph α} {n : } :
          G.CliqueFree n IsEmpty ( ↪g G)
          theorem SimpleGraph.not_cliqueFree_card_of_top_embedding {α : Type u_1} {G : SimpleGraph α} [Fintype α] (f : ↪g G) :
          ¬G.CliqueFree (Fintype.card α)
          @[simp]
          theorem SimpleGraph.cliqueFree_bot {α : Type u_1} {n : } (h : 2 n) :
          .CliqueFree n
          theorem SimpleGraph.CliqueFree.mono {α : Type u_1} {G : SimpleGraph α} {m : } {n : } (h : m n) :
          G.CliqueFree mG.CliqueFree n
          theorem SimpleGraph.CliqueFree.anti {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : } (h : G H) :
          H.CliqueFree nG.CliqueFree n
          theorem SimpleGraph.CliqueFree.comap {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : } {H : SimpleGraph β} (f : H ↪g G) :
          G.CliqueFree nH.CliqueFree n

          If a graph is cliquefree, any graph that embeds into it is also cliquefree.

          @[simp]
          theorem SimpleGraph.cliqueFree_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : } {f : α β} [Nonempty α] :
          (SimpleGraph.map f G).CliqueFree n G.CliqueFree n
          theorem SimpleGraph.cliqueFree_of_card_lt {α : Type u_1} {G : SimpleGraph α} {n : } [Fintype α] (hc : Fintype.card α < n) :
          G.CliqueFree n

          See SimpleGraph.cliqueFree_of_chromaticNumber_lt for a tighter bound.

          theorem SimpleGraph.cliqueFree_completeMultipartiteGraph {n : } {ι : Type u_3} [Fintype ι] (V : ιType u_4) (hc : Fintype.card ι < n) :

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

          theorem SimpleGraph.CliqueFree.replaceVertex {α : Type u_1} {G : SimpleGraph α} {n : } [DecidableEq α] (h : G.CliqueFree n) (s : α) (t : α) :
          (G.replaceVertex s t).CliqueFree n

          Clique-freeness is preserved by replaceVertex.

          @[simp]
          theorem SimpleGraph.cliqueFree_two {α : Type u_1} {G : SimpleGraph α} :
          G.CliqueFree 2 G =
          theorem SimpleGraph.CliqueFree.sup_edge {α : Type u_1} {G : SimpleGraph α} {n : } (h : G.CliqueFree n) (v : α) (w : α) :
          (G SimpleGraph.edge v w).CliqueFree (n + 1)

          Adding an edge increases the clique number by at most one.

          def SimpleGraph.CliqueFreeOn {α : Type u_1} (G : SimpleGraph α) (s : Set α) (n : ) :

          G.CliqueFreeOn s n means that G has no n-cliques contained in s.

          Equations
          • G.CliqueFreeOn s n = ∀ ⦃t : Finset α⦄, t s¬G.IsNClique n t
          Instances For
            theorem SimpleGraph.CliqueFreeOn.subset {α : Type u_1} (G : SimpleGraph α) {s₁ : Set α} {s₂ : Set α} {n : } (hs : s₁ s₂) (h₂ : G.CliqueFreeOn s₂ n) :
            G.CliqueFreeOn s₁ n
            theorem SimpleGraph.CliqueFreeOn.mono {α : Type u_1} (G : SimpleGraph α) {s : Set α} {m : } {n : } (hmn : m n) (hG : G.CliqueFreeOn s m) :
            G.CliqueFreeOn s n
            theorem SimpleGraph.CliqueFreeOn.anti {α : Type u_1} (G : SimpleGraph α) (H : SimpleGraph α) {s : Set α} {n : } (hGH : G H) (hH : H.CliqueFreeOn s n) :
            G.CliqueFreeOn s n
            @[simp]
            theorem SimpleGraph.cliqueFreeOn_empty {α : Type u_1} (G : SimpleGraph α) {n : } :
            G.CliqueFreeOn n n 0
            @[simp]
            theorem SimpleGraph.cliqueFreeOn_singleton {α : Type u_1} (G : SimpleGraph α) {a : α} {n : } :
            G.CliqueFreeOn {a} n 1 < n
            @[simp]
            theorem SimpleGraph.cliqueFreeOn_univ {α : Type u_1} (G : SimpleGraph α) {n : } :
            G.CliqueFreeOn Set.univ n G.CliqueFree n
            theorem SimpleGraph.CliqueFree.cliqueFreeOn {α : Type u_1} (G : SimpleGraph α) {s : Set α} {n : } (hG : G.CliqueFree n) :
            G.CliqueFreeOn s n
            theorem SimpleGraph.cliqueFreeOn_of_card_lt {α : Type u_1} (G : SimpleGraph α) {n : } {s : Finset α} (h : s.card < n) :
            G.CliqueFreeOn (↑s) n
            @[simp]
            theorem SimpleGraph.cliqueFreeOn_two {α : Type u_1} (G : SimpleGraph α) {s : Set α} :
            G.CliqueFreeOn s 2 s.Pairwise G.Adj
            theorem SimpleGraph.CliqueFreeOn.of_succ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {a : α} {n : } (hs : G.CliqueFreeOn s (n + 1)) (ha : a s) :
            G.CliqueFreeOn (s G.neighborSet a) n

            Set of cliques #

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

            The n-cliques in a graph as a set.

            Equations
            • G.cliqueSet n = {s : Finset α | G.IsNClique n s}
            Instances For
              @[simp]
              theorem SimpleGraph.mem_cliqueSet_iff {α : Type u_1} {G : SimpleGraph α} {n : } {s : Finset α} :
              s G.cliqueSet n G.IsNClique n s
              @[simp]
              theorem SimpleGraph.cliqueSet_eq_empty_iff {α : Type u_1} {G : SimpleGraph α} {n : } :
              G.cliqueSet n = G.CliqueFree n
              theorem SimpleGraph.CliqueFree.cliqueSet {α : Type u_1} {G : SimpleGraph α} {n : } :
              G.CliqueFree nG.cliqueSet n =

              Alias of the reverse direction of SimpleGraph.cliqueSet_eq_empty_iff.

              theorem SimpleGraph.cliqueSet_mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : } (h : G H) :
              G.cliqueSet n H.cliqueSet n
              theorem SimpleGraph.cliqueSet_mono' {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} (h : G H) :
              G.cliqueSet H.cliqueSet
              @[simp]
              theorem SimpleGraph.cliqueSet_zero {α : Type u_1} (G : SimpleGraph α) :
              G.cliqueSet 0 = {}
              @[simp]
              theorem SimpleGraph.cliqueSet_one {α : Type u_1} (G : SimpleGraph α) :
              G.cliqueSet 1 = Set.range singleton
              @[simp]
              theorem SimpleGraph.cliqueSet_bot {α : Type u_1} {n : } (hn : 1 < n) :
              .cliqueSet n =
              @[simp]
              theorem SimpleGraph.cliqueSet_map {α : Type u_1} {β : Type u_2} {n : } (hn : n 1) (G : SimpleGraph α) (f : α β) :
              (SimpleGraph.map f G).cliqueSet n = Finset.map f '' G.cliqueSet n
              @[simp]
              theorem SimpleGraph.cliqueSet_map_of_equiv {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (e : α β) (n : ) :
              (SimpleGraph.map e.toEmbedding G).cliqueSet n = Finset.map e.toEmbedding '' G.cliqueSet n

              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.

              Equations
              Instances For
                @[simp]
                theorem SimpleGraph.mem_cliqueFinset_iff {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } {s : Finset α} :
                s G.cliqueFinset n G.IsNClique n s
                @[simp]
                theorem SimpleGraph.coe_cliqueFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (n : ) :
                (G.cliqueFinset n) = G.cliqueSet n
                @[simp]
                theorem SimpleGraph.cliqueFinset_eq_empty_iff {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } :
                G.cliqueFinset n = G.CliqueFree n
                theorem SimpleGraph.CliqueFree.cliqueFinset {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } :
                G.CliqueFree nG.cliqueFinset n =

                Alias of the reverse direction of SimpleGraph.cliqueFinset_eq_empty_iff.

                theorem SimpleGraph.card_cliqueFinset_le {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } :
                (G.cliqueFinset n).card (Fintype.card α).choose n
                theorem SimpleGraph.cliqueFinset_mono {α : Type u_1} {G : SimpleGraph α} (H : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } [DecidableRel H.Adj] (h : G H) :
                G.cliqueFinset n H.cliqueFinset n
                @[simp]
                theorem SimpleGraph.cliqueFinset_map {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : } [Fintype β] [DecidableEq β] (f : α β) (hn : n 1) :
                (SimpleGraph.map f G).cliqueFinset n = Finset.map { toFun := Finset.map f, inj' := } (G.cliqueFinset n)
                @[simp]
                theorem SimpleGraph.cliqueFinset_map_of_equiv {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Fintype β] [DecidableEq β] (e : α β) (n : ) :
                (SimpleGraph.map e.toEmbedding G).cliqueFinset n = Finset.map { toFun := Finset.map e.toEmbedding, inj' := } (G.cliqueFinset n)