Database
GRAPH THEORY
Walks, paths and cycles
Walks
relwlk
Metamath Proof Explorer
Description: The set ( Walks G ) of all walks on G is a set of pairs by
our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens , 30-Jun-2018) (Revised by AV , 19-Feb-2021)
Ref
Expression
Assertion
relwlk
⊢ Rel ⁡ Walks ⁡ G
Proof
Step
Hyp
Ref
Expression
1
df-wlks
⊢ Walks = g ∈ V ⟼ f p | f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
2
1
relmptopab
⊢ Rel ⁡ Walks ⁡ G