edges_nodup_of_support_nodup — Mathlib

English

If p.support is Nodup, then p.edges is Nodup.

Русский

Если p.support имеет Nodup, то p.edges также Nodup.

LaTeX

$$$ p.\mathrm{support}.\mathrm{Nodup} \Rightarrow p.\mathrm{edges}.\mathrm{Nodup} $$$

Lean4

theorem edges_nodup_of_support_nodup {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.edges.Nodup := by
  induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
    exact ⟨fun h' => h.1 (fst_mem_support_of_mem_edges p' h'), ih h.2⟩

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