Theorems · Definition · combinatorics
SimpleGraph.Embedding.completeGraph
{α : Type u_5} → {β : Type u_6} → (α ↪ β) → SimpleGraph.completeGraph α ↪g SimpleGraph.completeGraph βEmbeddings of types induce embeddings of complete graphs on those types.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Maps
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Function.Embeddingstatement and proof · cited by 988
- SimpleGraph.completeGraphstatement · cited by 49
- SimpleGraph.Embeddingstatement · cited by 41
Cited by11
Results whose statement or proof uses this declaration.
- SimpleGraph.topEmbeddingOfNotCliqueFreeproof · cited by 2
- SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infiniteproof · cited by 2
- SimpleGraph.recolorOfEmbeddingproof · cited by 1
- SimpleGraph.isContained_top_iffproof · cited by 0
- SimpleGraph.Iso.toEmbedding_completeGraphstatement · cited by 0
- SimpleGraph.Embedding.coe_completeGraphstatement · cited by 0
- SimpleGraph.coe_recolorOfCardLEstatement · cited by 0
- SimpleGraph.coe_recolorOfEmbeddingstatement · cited by 0
- SimpleGraph.coe_recolorOfEquivstatement · cited by 0
- SimpleGraph.top_isIndContained_top_iffproof · cited by 0
- SimpleGraph.colorable_iff_exists_bdd_nat_coloringproof · cited by 0