finsetWalkLengthLT — Mathlib

English

The finset of walks from u to v with length strictly less than n is the union of the length-l finsets for l < n.

Русский

Множество ходов длины строго меньше n равно объединению множеств ходов длины l для всех l < n.

LaTeX

$$def finsetWalkLengthLT (n : ℕ) (u v : V) : Finset (G.Walk u v)$$

Lean4

/-- The `Finset` of walks from `u` to `v` with length less than `n`. See `finsetWalkLength` for
context. In particular, we use this definition for `SimpleGraph.Path.instFintype`. -/
def finsetWalkLengthLT (n : ℕ) (u v : V) : Finset (G.Walk u v) :=
  (Finset.range n).disjiUnion (fun l ↦ G.finsetWalkLength l u v)
    (fun l _ l' _ hne _ hsl hsl' p hp ↦
      have hl : p.length = l := mem_finsetWalkLength_iff.mp (hsl hp)
      have hl' : p.length = l' := mem_finsetWalkLength_iff.mp (hsl' hp)
      False.elim <| hne <| hl.symm.trans hl')

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