count_support_takeUntil_eq_one — Mathlib

English

For two vertices, reachability is equivalent to the existence of a finite-length path-walk to connect them.

Русский

Для двух вершин достижимость эквивалентна существованию конечной длины пути между ними.

LaTeX

$$$G.Reachable(u,v) \iff \exists n : Fin (Fintype.card V), (G.finsetWalkLength n u v).Nonempty$$$

Lean4

@[simp]
theorem count_support_takeUntil_eq_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.takeUntil u h).support.count u = 1 := by
  induction p
  · rw [mem_support_nil_iff] at h
    subst u
    simp
  · cases h
    · simp
    · simp! only
      split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

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