English
A bijective graph morphism maps a Hamiltonian cycle to a Hamiltonian cycle (alternative form of the previous theorem).
Русский
Биекция графа отображает гамильтонов цикл в гамильтонов цикл (альтернативная формулировка).
LaTeX
$$$$f\text{ bijective} \Rightarrow p.IsHamiltonianCycle \Rightarrow (p.map f).IsHamiltonianCycle.$$$$
Lean4
theorem map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f) (hp : p.IsHamiltonianCycle) :
(p.map f).IsHamiltonianCycle where
toIsCycle := hp.isCycle.map hf.injective
isHamiltonian_tail := by
simp only [IsHamiltonian, hf.surjective.forall]
intro x
rcases p with (_ | ⟨y, p⟩)
· cases hp.ne_nil rfl
simp only [map_cons, getVert_cons_succ, tail_cons, support_copy, support_map]
rw [List.count_map_of_injective _ _ hf.injective]
simpa using hp.isHamiltonian_tail x
