count_edges_takeUntil_le_one — Mathlib

English

In the initial segment up to the first occurrence of a vertex u in a walk, the number of edges labeled {u,x} between u and a fixed x is at most 1 for each x.

Русский

В начальном отрезке до первого появления вершины u в пути число рёбер вида {u,x} равно либо 0, либо 1 для каждого x.

LaTeX

$$$\text{List.count} (\text{Sym2.mk} \{ \ fst := u, \ snd := x \}) (p.takeUntil u h).edges \le 1$$$

Lean4

theorem count_edges_takeUntil_le_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) :
    (p.takeUntil u h).edges.count s(u, x) ≤ 1 := by
  induction p with
  | nil =>
    rw [mem_support_nil_iff] at h
    subst u
    simp
  | cons ha p' ih =>
    cases h
    · simp
    · simp! only
      split_ifs with h'
      · subst h'
        simp
      · rw [edges_cons, List.count_cons]
        split_ifs with h''
        · simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''
          obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
          · exact (h' rfl).elim
          · cases p' <;> simp!
        · apply ih

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