fintypeSetPathLength — Mathlib

English

In a locally finite simple graph with decidable equality on vertices, for any two vertices u, v and any natural number n, the set of walks from u to v that are paths of length n is finite.

Русский

Для локально конечного простого графа с заданной равенством вершин, для любых вершин u, v и любого натурального числа n множество путей p из u в v, удовлетворяющих условию, что p является путём и имеет длину n, конечно.

LaTeX

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

Lean4

instance fintypeSetPathLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v | p.IsPath ∧ p.length = n} :=
  Fintype.ofFinset ({w ∈ G.finsetWalkLength n u v | w.IsPath}) <| by simp [mem_finsetWalkLength_iff, and_comm]

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