English
The set of length-n walks, viewed as a Set, coincides with the set of walks whose length equals n.
Русский
Множество ходов длины n, рассматриваемое как множество, совпадает с множеством ходов, у которых длина равна n.
LaTeX
$$(G.finsetWalkLength n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}$$
Lean4
theorem coe_finsetWalkLength_eq (n : ℕ) (u v : V) :
(G.finsetWalkLength n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n} := by
induction n generalizing u v with
| zero => obtain rfl | huv := eq_or_ne u v <;> simp [finsetWalkLength, set_walk_length_zero_eq_of_ne, *]
| succ n
ih =>
simp only [finsetWalkLength, set_walk_length_succ_eq, Finset.coe_biUnion, Finset.mem_coe, Finset.mem_univ,
Set.iUnion_true]
ext p
simp only [mem_neighborSet, Finset.coe_map, Embedding.coeFn_mk, Set.iUnion_coe_set, Set.mem_iUnion, Set.mem_image,
Finset.mem_coe, Set.mem_setOf_eq]
congr!
rename_i w _ q
have := Set.ext_iff.mp (ih w v) q
simp only [Finset.mem_coe, Set.mem_setOf_eq] at this
rw [← this]
