darts_nodup_of_support_nodup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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