Theorems · Definition · combinatorics
SimpleGraph.Copy.toEmbedding
{α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → α ↪ βA copy gives rise to an embedding of vertex types.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Copy
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- SimpleGraphstatement and proof · cited by 3,072
- Function.Embeddingstatement · cited by 988
- SimpleGraph.Copystatement and proof · cited by 49
- SimpleGraph.Copy.injectiveproof · cited by 3
Cited by11
Results whose statement or proof uses this declaration.
- SimpleGraph.Copy.topEmbeddingproof · cited by 4
- SimpleGraph.IsContained.not_cliqueFreeproof · cited by 3
- SimpleGraph.UnitDistEmbedding.copyproof · cited by 1
- SimpleGraph.bot_isContained_iff_card_leproof · cited by 1
- SimpleGraph.isNClique_map_copy_topstatement and proof · cited by 1
- SimpleGraph.isContained_iff_exists_le_comapproof · cited by 0
- SimpleGraph.isContained_top_iffproof · cited by 0
- SimpleGraph.UnitDistEmbedding.copy_p_applystatement · cited by 0
- SimpleGraph.UnitDistEmbedding.embed_p_applystatement · cited by 0
- SimpleGraph.UnitDistEmbedding.iso_p_applystatement · cited by 0
- SimpleGraph.cliqueFree_of_card_ltproof · cited by 0