map_isTrail_iff_of_injective — Mathlib

English

If e is in the edges of p, then e occurs exactly once in (p.map f).edges, under the appropriate injectivity and IsPath assumptions.

Русский

Если ребро e принадлежит граням p, то оно встречается ровно один раз в гранях (p.map f), при соответствующих предпосылках на инъективность и IsPath.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Path u v} (e : Sym2 V) (hw : e \in (p : G.Walk u v).edges), (p : G.Walk u v).edges.count e = 1$$$

Lean4

theorem map_isTrail_iff_of_injective (hinj : Function.Injective f) : (p.map f).IsTrail ↔ p.IsTrail := by
  induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [map_cons, cons_isTrail_iff, ih, cons_isTrail_iff]
    apply and_congr_right'
    rw [← Sym2.map_pair_eq, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]

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