coe_finsetWalkLengthLT_eq — Mathlib

English

The finset of walks of length less than n corresponds to the set of walks with length less than n.

Русский

Множество ходов длины менее n соответствует множеству ходов длины менее n.

LaTeX

$$coe_finsetWalkLengthLT_eq (n) (u) (v) : (G.finsetWalkLengthLT n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length < n}$$

Lean4

theorem coe_finsetWalkLengthLT_eq (n : ℕ) (u v : V) :
    (G.finsetWalkLengthLT n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length < n} :=
  by
  ext p
  simp [finsetWalkLengthLT, mem_coe, mem_finsetWalkLength_iff]

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