take_spec — Mathlib

English

The subtype of walks from u to v that are paths and have length strictly less than n is finite.

Русский

Подтип путей между вершинами u и v, являющихся путями и имеющих длину строго меньше n, конечен.

LaTeX

$$$\left| \{ p : G.Walk(u,v) \mid p.IsPath \land p.length < n \} \right| < \infty$$

Lean4

/-- The `takeUntil` and `dropUntil` functions split a walk into two pieces.
The lemma `SimpleGraph.Walk.count_support_takeUntil_eq_one` specifies where this split occurs. -/
@[simp]
theorem take_spec {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).append (p.dropUntil u h) = p :=
  by
  induction p
  · rw [mem_support_nil_iff] at h
    subst u
    rfl
  · cases h
    · simp!
    · simp! only
      split_ifs with h' <;> subst_vars <;> simp [*]

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