Theorems · Definition · combinatorics

SimpleGraph.Embedding.comp

{V : Type u_1} →
  {W : Type u_2} →
    {X : Type u_3} → {G : SimpleGraph V} → {G' : SimpleGraph W} → {G'' : SimpleGraph X} → G' ↪g G'' → G ↪g G' → G ↪g G''

Composition of graph embeddings.

Defined in: Mathlib.Combinatorics.SimpleGraph.Maps
Cited by: 10 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

SimpleGraphstatement and proof · cited by 3,072
SimpleGraph.Embeddingstatement and proof · cited by 41
RelEmbedding.transproof · cited by 27

Cited by11

Results whose statement or proof uses this declaration.

SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infiniteproof · cited by 2
SimpleGraph.topEmbeddingOfNotCliqueFreeproof · cited by 2
SimpleGraph.IsIndContained.transproof · cited by 1
SimpleGraph.Embedding.refl_compstatement · cited by 0
SimpleGraph.Embedding.coe_compstatement · cited by 0
SimpleGraph.Embedding.sum_comp_sumCommstatement · cited by 0
SimpleGraph.Embedding.sum_sum_comp_sumAssocstatement · cited by 0
SimpleGraph.Embedding.comp_assocstatement · cited by 0
SimpleGraph.Embedding.comp_reflstatement · cited by 0
SimpleGraph.isIndContained_iff_exists_iso_induceproof · cited by 0
SimpleGraph.IsCompleteMultipartite.comapproof · cited by 0