Documentation

Mathlib.Combinatorics.SimpleGraph.Copy

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.

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.

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

Instances For

@[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 : α ↪ β) :

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) :

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) :

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 β) :

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.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.

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.

@[reducible, inline]

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

The proposition that a simple graph does not contain a copy of another simple graph.

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 ≠ ⊥) :

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) :

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.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.

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.