Containment of graphs

This file introduces the concept of one simple graph containing a copy of another.

For two simple graph G and H, a copy of G in H is a (not necessarily induced) subgraph of H isomorphic to G.

If there exists a copy of G in H, we say that H contains G. This is equivalent to saying that there is an injective graph homomorphism G → H them (this is not the same as a graph embedding, as we do not require the subgraph to be induced).

If there exists an induced copy of G in H, we say that H inducingly contains G. This is equivalent to saying that there is a graph embedding G ↪ H.

Main declarations

Containment:

• SimpleGraph.Copy G H is the type of copies of G in H, implemented as the subtype of injective homomorphisms.
• SimpleGraph.IsContained G H, G ⊑ H is the relation that H contains a copy of G, that is, the type of copies of G in H is nonempty. This is equivalent to the existence of an isomorphism from G to a subgraph of H. This is similar to SimpleGraph.IsSubgraph except that the simple graphs here need not have the same underlying vertex type.
• SimpleGraph.Free is the predicate that H is G-free, that is, H does not contain a copy of G. This is the negation of SimpleGraph.IsContained implemented for convenience.
• SimpleGraph.killCopies G H: Subgraph of G that does not contain H. Obtained by arbitrarily removing an edge from each copy of H in G.
• SimpleGraph.copyCount G H: Number of copies of H in G, ie number of subgraphs of G isomorphic to H.
• SimpleGraph.labelledCopyCount G H: Number of labelled copies of H in G, ie number of graph embeddings from H to G.

Induced containment:

• Induced copies of G inside H are already defined as G ↪g H.
• SimpleGraph.IsIndContained G H : G is contained as an induced subgraph in H.

Notation

The following notation is declared in locale SimpleGraph:

• G ⊑ H for SimpleGraph.IsContained G H.
• G ⊴ H for SimpleGraph.IsIndContained G H.

TODO

• Relate ⊤ ⊑ H/⊥ ⊑ H to there being a clique/independent set in H.
• Count induced copies of a graph inside another.
• Make copyCount/labelledCopyCount computable (not necessarily efficiently).

Copies

Not necessarily induced copies

A copy of a subgraph G inside a subgraph H is an embedding of the vertices of G into the vertices of H, such that adjacency in G implies adjacency in H.

We capture this concept by injective graph homomorphisms.

structure SimpleGraph.Copy {α : Type u_4} {β : Type u_5} (A : SimpleGraph α) (B : SimpleGraph β) : Type (max u_4 u_5)

The type of copies as a subtype of injective homomorphisms.

• toHom : A →g B

  A copy gives rise to a homomorphism.

• injective' : Function.Injective ⇑self.toHom

@[reducible, inline]

abbrev SimpleGraph.Hom.toCopy {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A →g B) (h : Function.Injective ⇑f) : A.Copy B

An injective homomorphism gives rise to a copy.

Equations

• f.toCopy h = { toHom := f, injective' := h }

@[reducible, inline]

abbrev SimpleGraph.Embedding.toCopy {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A ↪g B) : A.Copy B

An embedding gives rise to a copy.

Equations

• f.toCopy = f.toHom.toCopy ⋯

@[reducible, inline]

abbrev SimpleGraph.Iso.toCopy {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A ≃g B) : A.Copy B

An isomorphism gives rise to a copy.

Equations

• f.toCopy = f.toEmbedding.toCopy

instance SimpleGraph.Copy.instFunLike {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : FunLike (A.Copy B) α β

Equations

• SimpleGraph.Copy.instFunLike = { coe := fun (f : A.Copy B) => ⇑f.toHom, coe_injective' := ⋯ }

theorem SimpleGraph.Copy.injective {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : Function.Injective ⇑f.toHom

theorem SimpleGraph.Copy.ext {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {f g : A.Copy B} : (∀ (a : α), f a = g a) → f = g

@[simp]

theorem SimpleGraph.Copy.coe_toHom {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : ⇑f.toHom = ⇑f

@[simp]

theorem SimpleGraph.Copy.toHom_apply {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α) : f.toHom a = f a

@[simp]

theorem SimpleGraph.Copy.coe_mk {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A →g B) (hf : Function.Injective ⇑f) : ⇑{ toHom := f, injective' := hf } = ⇑f

@[deprecated SimpleGraph.Copy.toHom_apply (since := "2025-03-19")]

theorem SimpleGraph.Copy.coe_toHom_apply {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α) : f.toHom a = f a

Alias of SimpleGraph.Copy.toHom_apply.

def SimpleGraph.Copy.mapEdgeSet {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : ↑A.edgeSet ↪ ↑B.edgeSet

A copy induces an embedding of edge sets.

Equations

• f.mapEdgeSet = { toFun := f.toHom.mapEdgeSet, inj' := ⋯ }

def SimpleGraph.Copy.mapNeighborSet {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α) : ↑(A.neighborSet a) ↪ ↑(B.neighborSet (f a))

A copy induces an embedding of neighbor sets.

Equations

• f.mapNeighborSet a = { toFun := fun (v : ↑(A.neighborSet a)) => ⟨f ↑v, ⋯⟩, inj' := ⋯ }

def SimpleGraph.Copy.toEmbedding {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : α ↪ β

A copy gives rise to an embedding of vertex types.

Equations

• f.toEmbedding = { toFun := ⇑f, inj' := ⋯ }

def SimpleGraph.Copy.id {V : Type u_1} (G : SimpleGraph V) : G.Copy G

The identity copy from a simple graph to itself.

Equations

• SimpleGraph.Copy.id G = { toHom := SimpleGraph.Hom.id, injective' := ⋯ }

@[simp]

theorem SimpleGraph.Copy.coe_id {V : Type u_1} {G : SimpleGraph V} : ⇑(id G) = _root_.id

def SimpleGraph.Copy.comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) : A.Copy C

The composition of copies is a copy.

Equations

• g.comp f = { toHom := g.toHom.comp f.toHom, injective' := ⋯ }

@[simp]

theorem SimpleGraph.Copy.comp_apply {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) (a : α) : (g.comp f) a = g (f a)

def SimpleGraph.Copy.ofLE {V : Type u_1} (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : G₁.Copy G₂

The copy from a subgraph to the supergraph.

Equations

• SimpleGraph.Copy.ofLE G₁ G₂ h = { toHom := SimpleGraph.Hom.ofLE h, injective' := ⋯ }

@[simp]

theorem SimpleGraph.Copy.coe_comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem SimpleGraph.Copy.coe_ofLE {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : ⇑(ofLE G₁ G₂ h) = _root_.id

@[simp]

theorem SimpleGraph.Copy.ofLE_refl {V : Type u_1} {G : SimpleGraph V} : ofLE G G ⋯ = id G

@[simp]

theorem SimpleGraph.Copy.ofLE_comp {V : Type u_1} {G₁ G₂ G₃ : SimpleGraph V} (h₁₂ : G₁ ≤ G₂) (h₂₃ : G₂ ≤ G₃) : (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯

def SimpleGraph.Copy.induce {V : Type u_1} (G : SimpleGraph V) (s : Set V) : (SimpleGraph.induce s G).Copy G

The copy from an induced subgraph to the initial simple graph.

Equations

• SimpleGraph.Copy.induce G s = (SimpleGraph.Embedding.induce s).toCopy

def SimpleGraph.Copy.bot {α : Type u_4} {β : Type u_5} {B : SimpleGraph β} (f : α ↪ β) : ⊥.Copy B

The copy of ⊥ in any simple graph that can embed its vertices.

Equations

• SimpleGraph.Copy.bot f = { toHom := { toFun := ⇑f, map_rel' := ⋯ }, injective' := ⋯ }

noncomputable def SimpleGraph.Copy.isoSubgraphMap {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (A' : A.Subgraph) : A'.coe ≃g (Subgraph.map f.toHom A').coe

The isomorphism from a subgraph of A to its map under a copy f : Copy A B.

Equations

• f.isoSubgraphMap A' = { toEquiv := Equiv.Set.image (⇑f.toHom) A'.verts ⋯, map_rel_iff' := ⋯ }

@[reducible, inline]

abbrev SimpleGraph.Copy.toSubgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : B.Subgraph

The subgraph of B corresponding to a copy of A inside B.

Equations

• f.toSubgraph = SimpleGraph.Subgraph.map f.toHom ⊤

noncomputable def SimpleGraph.Copy.isoToSubgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : A ≃g f.toSubgraph.coe

The isomorphism from A to its copy under f : Copy A B.

Equations

• f.isoToSubgraph = (f.isoSubgraphMap ⊤).comp SimpleGraph.Subgraph.topIso.symm

@[simp]

theorem SimpleGraph.Copy.range_toSubgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : Set.range toSubgraph = {B' : B.Subgraph | Nonempty (A ≃g B'.coe)}

theorem SimpleGraph.Copy.toSubgraph_surjOn {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : Set.SurjOn toSubgraph Set.univ {B' : B.Subgraph | Nonempty (A ≃g B'.coe)}

instance SimpleGraph.Copy.instSubsingletonOfForall {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Subsingleton (V → W)] : Subsingleton (G.Copy H)

instance SimpleGraph.Copy.instFintypeOfSubtypeHomInjectiveCoe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype { f : G →g H // Function.Injective ⇑f }] : Fintype (G.Copy H)

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Subgraph.coeCopy {V : Type u_1} {G : SimpleGraph V} (G' : G.Subgraph) : G'.coe.Copy G

A Subgraph G gives rise to a copy from the coercion to G.

Equations

• G'.coeCopy = G'.hom.toCopy ⋯

Induced copies

An induced copy of a graph G inside a graph H is an embedding from the vertices of G into the vertices of H which preserves the adjacency relation.

This is already captured by the notion of graph embeddings, defined as G ↪g H.

Containment

Not necessarily induced containment

A graph H contains a graph G if there is some copy f : Copy G H of G inside H. This amounts to H having a subgraph isomorphic to G.

We denote "G is contained in H" by G ⊑ H (\squb).

@[reducible, inline]

abbrev SimpleGraph.IsContained {α : Type u_4} {β : Type u_5} (A : SimpleGraph α) (B : SimpleGraph β) : Prop

The relation IsContained A B, A ⊑ B says that B contains a copy of A.

This is equivalent to the existence of an isomorphism from A to a subgraph of B.

Equations

• A.IsContained B = Nonempty (A.Copy B)

def SimpleGraph.«term_⊑_» : Lean.TrailingParserDescr

The relation IsContained A B, A ⊑ B says that B contains a copy of A.

This is equivalent to the existence of an isomorphism from A to a subgraph of B.

Equations

• SimpleGraph.«term_⊑_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_⊑_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

theorem SimpleGraph.IsContained.refl {V : Type u_1} (G : SimpleGraph V) : G.IsContained G

A simple graph contains itself.

theorem SimpleGraph.IsContained.rfl {V : Type u_1} {G : SimpleGraph V} : G.IsContained G

theorem SimpleGraph.IsContained.of_le {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : G₁.IsContained G₂

A simple graph contains its subgraphs.

theorem SimpleGraph.IsContained.trans {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} : A.IsContained B → B.IsContained C → A.IsContained C

If A contains B and B contains C, then A contains C.

theorem SimpleGraph.IsContained.trans' {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} : B.IsContained C → A.IsContained B → A.IsContained C

If B contains C and A contains B, then A contains C.

theorem SimpleGraph.IsContained.mono_right {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B B' : SimpleGraph β} (h_isub : A.IsContained B) (h_sub : B ≤ B') : A.IsContained B'

theorem SimpleGraph.IsContained.trans_le {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B B' : SimpleGraph β} (h_isub : A.IsContained B) (h_sub : B ≤ B') : A.IsContained B'

Alias of SimpleGraph.IsContained.mono_right.

theorem SimpleGraph.IsContained.mono_left {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A'.IsContained B) : A.IsContained B

theorem SimpleGraph.IsContained.trans_le' {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A'.IsContained B) : A.IsContained B

Alias of SimpleGraph.IsContained.mono_left.

theorem SimpleGraph.isContained_congr {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (e : A ≃g B) : A.IsContained C ↔ B.IsContained C

If A ≃g B, then A is contained in C if and only if B is contained in C.

theorem SimpleGraph.IsContained.of_isEmpty {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} [IsEmpty α] : A.IsContained B

A simple graph having no vertices is contained in any simple graph.

theorem SimpleGraph.bot_isContained_iff_card_le {α : Type u_4} {β : Type u_5} {B : SimpleGraph β} [Fintype α] [Fintype β] : ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β

⊥ is contained in any simple graph having sufficently many vertices.

theorem SimpleGraph.IsContained.bot {α : Type u_4} {β : Type u_5} {B : SimpleGraph β} [Fintype α] [Fintype β] : ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β

Alias of SimpleGraph.bot_isContained_iff_card_le.

---

⊥ is contained in any simple graph having sufficently many vertices.

theorem SimpleGraph.Subgraph.coe_isContained {V : Type u_1} {G : SimpleGraph V} (G' : G.Subgraph) : G'.coe.IsContained G

A simple graph G contains all Subgraph G coercions.

@[deprecated SimpleGraph.Copy.isoSubgraphMap (since := "2025-03-19")]

def SimpleGraph.Subgraph.Copy.map {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (A' : A.Subgraph) : A'.coe ≃g (Subgraph.map f.toHom A').coe

Alias of SimpleGraph.Copy.isoSubgraphMap.

---

The isomorphism from a subgraph of A to its map under a copy f : Copy A B.

Equations

• @SimpleGraph.Subgraph.Copy.map = @SimpleGraph.Copy.isoSubgraphMap

theorem SimpleGraph.isContained_iff_exists_iso_subgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : A.IsContained B ↔ ∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

theorem SimpleGraph.IsContained.exists_iso_subgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : A.IsContained B → ∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)

Alias of the forward direction of SimpleGraph.isContained_iff_exists_iso_subgraph.

---

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

theorem SimpleGraph.IsContained.of_exists_iso_subgraph {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : (∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)) → A.IsContained B

Alias of the reverse direction of SimpleGraph.isContained_iff_exists_iso_subgraph.

---

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

@[reducible, inline]

abbrev SimpleGraph.Free {α : Type u_4} {β : Type u_5} (A : SimpleGraph α) (B : SimpleGraph β) : Prop

A.Free B means that B does not contain a copy of A.

Equations

• A.Free B = ¬A.IsContained B

theorem SimpleGraph.not_free {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} : ¬A.Free B ↔ A.IsContained B

theorem SimpleGraph.free_congr {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (e : A ≃g B) : A.Free C ↔ B.Free C

If A ≃g B, then C is A-free if and only if C is B-free.

theorem SimpleGraph.free_bot {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} (h : A ≠ ⊥) : A.Free ⊥

Induced containment

A graph H inducingly contains a graph G if there is some graph embedding G ↪ H. This amounts to H having an induced subgraph isomorphic to G.

We denote "G is inducingly contained in H" by G ⊴ H (\trianglelefteq).

def SimpleGraph.IsIndContained {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) : Prop

A simple graph G is inducingly contained in a simple graph H if there exists an induced subgraph of H isomorphic to G. This is denoted by G ⊴ H.

Equations

• G.IsIndContained H = Nonempty (G ↪g H)

def SimpleGraph.«term_⊴_» : Lean.TrailingParserDescr

A simple graph G is inducingly contained in a simple graph H if there exists an induced subgraph of H isomorphic to G. This is denoted by G ⊴ H.

Equations

• SimpleGraph.«term_⊴_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_⊴_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊴ ") (Lean.ParserDescr.cat `term 51))

theorem SimpleGraph.IsIndContained.isContained {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : G.IsIndContained H → G.IsContained H

theorem SimpleGraph.Iso.isIndContained {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) : G.IsIndContained H

If G is isomorphic to H, then G is inducingly contained in H.

theorem SimpleGraph.Iso.isIndContained' {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) : H.IsIndContained G

If G is isomorphic to H, then H is inducingly contained in G.

theorem SimpleGraph.Subgraph.IsInduced.isIndContained {V : Type u_1} {G : SimpleGraph V} {G' : G.Subgraph} (hG' : G'.IsInduced) : G'.coe.IsIndContained G

theorem SimpleGraph.IsIndContained.refl {V : Type u_1} (G : SimpleGraph V) : G.IsIndContained G

theorem SimpleGraph.IsIndContained.rfl {V : Type u_1} {G : SimpleGraph V} : G.IsIndContained G

theorem SimpleGraph.IsIndContained.trans {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph X} : G.IsIndContained H → H.IsIndContained I → G.IsIndContained I

theorem SimpleGraph.IsIndContained.of_isEmpty {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [IsEmpty V] : G.IsIndContained H

theorem SimpleGraph.isIndContained_iff_exists_iso_subgraph {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : G.IsIndContained H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced

theorem SimpleGraph.IsIndContained.exists_iso_subgraph {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : G.IsIndContained H → ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced

Alias of the forward direction of SimpleGraph.isIndContained_iff_exists_iso_subgraph.

theorem SimpleGraph.IsIndContained.of_exists_iso_subgraph {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : (∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced) → G.IsIndContained H

Alias of the reverse direction of SimpleGraph.isIndContained_iff_exists_iso_subgraph.

@[simp]

theorem SimpleGraph.top_isIndContained_iff_top_isContained {V : Type u_1} {W : Type u_2} {H : SimpleGraph W} : ⊤.IsIndContained H ↔ ⊤.IsContained H

@[simp]

theorem SimpleGraph.compl_isIndContained_compl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : Gᶜ.IsIndContained Hᶜ ↔ G.IsIndContained H

theorem SimpleGraph.IsIndContained.of_compl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : Gᶜ.IsIndContained Hᶜ → G.IsIndContained H

Alias of the forward direction of SimpleGraph.compl_isIndContained_compl.

theorem SimpleGraph.IsIndContained.compl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : G.IsIndContained H → Gᶜ.IsIndContained Hᶜ

Alias of the reverse direction of SimpleGraph.compl_isIndContained_compl.

Counting the copies

If G and H are finite graphs, we can count the number of unlabelled and labelled copies of G in H.

Not necessarily induced copies

noncomputable def SimpleGraph.labelledCopyCount {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (G : SimpleGraph V) (H : SimpleGraph W) : ℕ

G.labelledCopyCount H is the number of labelled copies of H in G, i.e. the number of graph embeddings from H to G. See SimpleGraph.copyCount for the number of unlabelled copies.

Equations

• G.labelledCopyCount H = Fintype.card (H.Copy G)

@[simp]

theorem SimpleGraph.labelledCopyCount_of_isEmpty {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) : G.labelledCopyCount H = 1

@[simp]

theorem SimpleGraph.labelledCopyCount_eq_zero {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [Fintype W] : G.labelledCopyCount H = 0 ↔ H.Free G

@[simp]

theorem SimpleGraph.labelledCopyCount_pos {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [Fintype W] : 0 < G.labelledCopyCount H ↔ H.IsContained G

noncomputable def SimpleGraph.copyCount {V : Type u_1} {W : Type u_2} [Fintype V] (G : SimpleGraph V) (H : SimpleGraph W) : ℕ

G.copyCount H is the number of unlabelled copies of H in G, i.e. the number of subgraphs of G isomorphic to H. See SimpleGraph.labelledCopyCount for the number of labelled copies.

Equations

• G.copyCount H = {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}.card

theorem SimpleGraph.copyCount_eq_card_image_copyToSubgraph {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [Fintype { f : H →g G // Function.Injective ⇑f }] [DecidableEq G.Subgraph] : G.copyCount H = (Finset.image Copy.toSubgraph Finset.univ).card

@[simp]

theorem SimpleGraph.copyCount_eq_zero {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] : G.copyCount H = 0 ↔ H.Free G

@[simp]

theorem SimpleGraph.copyCount_pos {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] : 0 < G.copyCount H ↔ H.IsContained G

theorem SimpleGraph.copyCount_le_labelledCopyCount {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [Fintype W] : G.copyCount H ≤ G.labelledCopyCount H

There's at least as many labelled copies of H in G than unlabelled ones.

@[simp]

theorem SimpleGraph.copyCount_bot {V : Type u_1} [Fintype V] (G : SimpleGraph V) : G.copyCount ⊥ = 1

@[simp]

theorem SimpleGraph.copyCount_of_isEmpty {V : Type u_1} {W : Type u_2} [Fintype V] [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) : G.copyCount H = 1

Induced copies

TODO

Killing a subgraph

An important aspect of graph containment is that we can remove not too many edges from a graph H to get a graph H' that doesn't contain G.

Killing not necessarily induced copies

SimpleGraph.killCopies G H is a subgraph of G where an edge was removed from each copy of H in G. By construction, it doesn't contain H and has at most the number of copies of H edges less than G.

theorem SimpleGraph.killCopies_def {V : Type u_7} {W : Type u_8} (G : SimpleGraph V) (H : SimpleGraph W) : G.killCopies H = if hH : H = ⊥ then G else G.deleteEdges (⋃ (G' : G.Subgraph), ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})

@[irreducible]

noncomputable def SimpleGraph.killCopies {V : Type u_7} {W : Type u_8} (G : SimpleGraph V) (H : SimpleGraph W) : SimpleGraph V

G.killCopies H is a subgraph of G where an arbitrary edge was removed from each copy of H in G. By construction, it doesn't contain H (unless H had no edges) and has at most the number of copies of H edges less than G. See free_killCopies and le_card_edgeFinset_killCopies for these two properties.

Equations

• G.killCopies H = if hH : H = ⊥ then G else G.deleteEdges (⋃ (G' : G.Subgraph), ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})

theorem SimpleGraph.killCopies_le_left {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : G.killCopies H ≤ G

Removing an edge from G for each subgraph isomorphic to H results in a subgraph of G.

@[simp]

theorem SimpleGraph.killCopies_bot {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) : G.killCopies ⊥ = G

theorem SimpleGraph.killCopies_eq_left {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (hH : H ≠ ⊥) : G.killCopies H = G ↔ H.Free G

G.killCopies H has no effect on G if and only if G already contained no copies of H. See Free.killCopies_eq_left for the reverse implication with no assumption on H.

theorem SimpleGraph.Free.killCopies_eq_left {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (hHG : H.Free G) : G.killCopies H = G

theorem SimpleGraph.free_killCopies {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (hH : H ≠ ⊥) : H.Free (G.killCopies H)

Removing an edge from G for each subgraph isomorphic to H results in a graph that doesn't contain H.

noncomputable instance SimpleGraph.killCopies.edgeSet.instFintype {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype ↑G.edgeSet] : Fintype ↑(G.killCopies H).edgeSet

Equations

• SimpleGraph.killCopies.edgeSet.instFintype = Fintype.ofInjective (Set.inclusion ⋯) ⋯

theorem SimpleGraph.le_card_edgeFinset_killCopies {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype ↑G.edgeSet] [Fintype V] : G.edgeFinset.card - G.copyCount H ≤ (G.killCopies H).edgeFinset.card

Removing an edge from H for each subgraph isomorphic to G means that the number of edges we've removed is at most the number of copies of G in H.

theorem SimpleGraph.le_card_edgeFinset_killCopies_add_copyCount {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype ↑G.edgeSet] [Fintype V] : G.edgeFinset.card ≤ (G.killCopies H).edgeFinset.card + G.copyCount H

Removing an edge from H for each subgraph isomorphic to G means that the number of edges we've removed is at most the number of copies of G in H.

Killing induced copies

TODO