mem_finsetWalkLength_iff — Mathlib

English

A walk p has length n if and only if p belongs to the Finset of length-n walks from u to v.

Русский

Ход p имеет длину n тогда и только тогда, когда он принадлежит Finset ходов длины n от u к v.

LaTeX

$$p ∈ G.finsetWalkLength n u v ↔ p.length = n$$

Lean4

theorem mem_finsetWalkLength_iff {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLength n u v ↔ p.length = n :=
  Set.ext_iff.mp (G.coe_finsetWalkLength_eq n u v) p

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