card_set_walk_length_eq — Mathlib

English

The cardinality of the set of length-n walks equals the cardinality of the corresponding finset.

Русский

Кардинал множества ходов длины n равен кардиналу соответствующего конечного множества.

LaTeX

$$Fintype.card {p : G.Walk u v | p.length = n} = #(G.finsetWalkLength n u v)$$

Lean4

theorem card_set_walk_length_eq (u v : V) (n : ℕ) :
    Fintype.card {p : G.Walk u v | p.length = n} = #(G.finsetWalkLength n u v) :=
  Fintype.card_ofFinset (G.finsetWalkLength n u v) fun p => by rw [← Finset.mem_coe, coe_finsetWalkLength_eq]

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