fintypeSetPathLengthLT — Mathlib

English

For any u, v in V and n, the set of walks from u to v that are paths with length less than n is finite.

Русский

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

LaTeX

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

Lean4

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

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