Theorems · Theorem · combinatorics
SimpleGraph.Walk.IsHamiltonian.injective_of_isPath_map
∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {β : Type u_2} {H : SimpleGraph β} {a b : α}
{p : G.Walk a b} {f : G →g H}, p.IsHamiltonian → (SimpleGraph.Walk.map f p).IsPath → Function.Injective ⇑f- Cited by
- 0 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setproof · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement · cited by 1,346
- SimpleGraph.Walkstatement and proof · cited by 915
- Set.InjOnproof · cited by 543
- SimpleGraph.Walk.IsPathstatement and proof · cited by 140
- SimpleGraph.Homstatement and proof · cited by 139
- SimpleGraph.Walk.mapstatement and proof · cited by 66
- SimpleGraph.Walk.IsHamiltonianstatement and proof · cited by 25
- Set.injOn_univproof · cited by 4
- SimpleGraph.Walk.IsHamiltonian.setOfPred_supportproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.