set_walk_length_toFinset_eq — Mathlib

English

The equality between finsetWalkLength and the Set description extends to Set equality with lengths.

Русский

Равенство между finsetWalkLength и описанием через множество распространяется на равенство множеств по длине.

LaTeX

$$coe_finsetWalkLength_eq (n) (u) (v) : (G.finsetWalkLength n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}$$

Lean4

theorem set_walk_length_toFinset_eq (n : ℕ) (u v : V) :
    {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v := by
  simp [← coe_finsetWalkLength_eq]
    /- See `SimpleGraph.adjMatrix_pow_apply_eq_card_walk` for the cardinality in terms of the `n`th
    power of the adjacency matrix. -/

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