fintypeSetWalkLength — Mathlib

English

The set of length-n walks between u and v forms a finite type (a finite set) when G is finite.

Русский

Множество ходов длины n между вершинами u и v образует конечный тип (конечное множество) при конечном графе G.

LaTeX

$$Fintype.ofFinset (G.finsetWalkLength n u v)$$

Lean4

instance fintypeSetWalkLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v | p.length = n} :=
  Fintype.ofFinset (G.finsetWalkLength n u v) fun p => by rw [← Finset.mem_coe, coe_finsetWalkLength_eq]

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