Theorems · Definition · combinatorics
SimpleGraph.Copy.toHom
{α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → A →g BA copy gives rise to a homomorphism.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Copy
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
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.Homstatement · cited by 139
- SimpleGraph.Copystatement and proof · cited by 49
Cited by18
Results whose statement or proof uses this declaration.
- SimpleGraph.Copy.compproof · cited by 5
- SimpleGraph.Copy.toSubgraphproof · cited by 4
- SimpleGraph.Copy.injectivestatement · cited by 3
- SimpleGraph.isContained_iff_exists_iso_subgraphproof · cited by 3
- SimpleGraph.Copy.comp_applyproof · cited by 2
- SimpleGraph.IsContained.egirth_leproof · cited by 2
- SimpleGraph.isIndContained_iff_exists_iso_subgraphproof · cited by 2
- SimpleGraph.Copy.injective'statement · cited by 1
- SimpleGraph.Copy.isoSubgraphMapstatement and proof · cited by 1
- SimpleGraph.turanGraph_cliqueFreeproof · cited by 1
- SimpleGraph.cycleGraph_isContained_iffproof · cited by 1
- SimpleGraph.Copy.coe_toHomstatement · cited by 0