Description: Define the set of all (simple) cycles (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory) , 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex."
According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of Bollobas p. 5.
However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017) (Revised by AV, 31-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cycls | ⊢ Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccycls | ⊢ Cycles | |
| 1 | vg | ⊢ 𝑔 | |
| 2 | cvv | ⊢ V | |
| 3 | vf | ⊢ 𝑓 | |
| 4 | vp | ⊢ 𝑝 | |
| 5 | 3 | cv | ⊢ 𝑓 |
| 6 | cpths | ⊢ Paths | |
| 7 | 1 | cv | ⊢ 𝑔 |
| 8 | 7 6 | cfv | ⊢ ( Paths ‘ 𝑔 ) |
| 9 | 4 | cv | ⊢ 𝑝 |
| 10 | 5 9 8 | wbr | ⊢ 𝑓 ( Paths ‘ 𝑔 ) 𝑝 |
| 11 | cc0 | ⊢ 0 | |
| 12 | 11 9 | cfv | ⊢ ( 𝑝 ‘ 0 ) |
| 13 | chash | ⊢ ♯ | |
| 14 | 5 13 | cfv | ⊢ ( ♯ ‘ 𝑓 ) |
| 15 | 14 9 | cfv | ⊢ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) |
| 16 | 12 15 | wceq | ⊢ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) |
| 17 | 10 16 | wa | ⊢ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) |
| 18 | 17 3 4 | copab | ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } |
| 19 | 1 2 18 | cmpt | ⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |
| 20 | 0 19 | wceq | ⊢ Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |