map_isCycle_iff_of_injective — Mathlib

English

Under an injective f, (p.map f).IsCycle iff p.IsCycle.

Русский

При инъективном отображении f, (p.map f).IsCycle эквивалентно p.IsCycle.

LaTeX

$$$ \forall {V} {V'} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u : V} {p : G.Walk u u}, Function.Injective (RelHom.instFunLike.coe f) \to (p.map f).IsCycle p.IsCycle$$$

Lean4

theorem map_isCycle_iff_of_injective {p : G.Walk u u} (hinj : Function.Injective f) : (p.map f).IsCycle ↔ p.IsCycle :=
  by
  rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, Ne, map_eq_nil_iff, support_map, ← List.map_tail,
    List.nodup_map_iff hinj]

Похожие утверждения