Counting walks of a given length

Main definitions

• walkLengthTwoEquivCommonNeighbors: bijective correspondence between walks of length two from u to v and common neighbours of u and v. Note that u and v may be the same.
• finsetWalkLength: the Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

TODO: should this be extended further?

Walks of a given length

theorem SimpleGraph.set_walk_self_length_zero_eq {V : Type u} (G : SimpleGraph V) (u : V) : {p : G.Walk u u | p.length = 0} = {SimpleGraph.Walk.nil}

theorem SimpleGraph.set_walk_length_zero_eq_of_ne {V : Type u} (G : SimpleGraph V) {u : V} {v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅

theorem SimpleGraph.set_walk_length_succ_eq {V : Type u} (G : SimpleGraph V) (u : V) (v : V) (n : ℕ) : {p : G.Walk u v | p.length = n.succ} = ⋃ (w : V), ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' : G.Walk w v | p'.length = n}

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe {V : Type u} (G : SimpleGraph V) (u : V) (v : V) (w : ↑(G.commonNeighbors u v)) : ↑((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (SimpleGraph.Adj.toWalk ⋯).concat ⋯

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe {V : Type u} (G : SimpleGraph V) (u : V) (v : V) (p : { p : G.Walk u v // p.length = 2 }) : ↑((G.walkLengthTwoEquivCommonNeighbors u v) p) = (↑p).getVert 1

def SimpleGraph.walkLengthTwoEquivCommonNeighbors {V : Type u} (G : SimpleGraph V) (u : V) (v : V) : { p : G.Walk u v // p.length = 2 } ≃ ↑(G.commonNeighbors u v)

Walks of length two from u to v correspond bijectively to common neighbours of u and v. Note that u and v may be the same.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.finsetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u : V) (v : V) : Finset (G.Walk u v)

The Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

See SimpleGraph.coe_finsetWalkLength_eq for the relationship between this Finset and the set of length-n walks.

Equations

• One or more equations did not get rendered due to their size.
• G.finsetWalkLength 0 u v = if h : u = v then ⋯ ▸ {SimpleGraph.Walk.nil} else ∅

theorem SimpleGraph.coe_finsetWalkLength_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u : V) (v : V) : ↑(G.finsetWalkLength n u v) = {p : G.Walk u v | p.length = n}

theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : ℕ} {u : V} {v : V} (p : G.Walk u v) : p ∈ G.finsetWalkLength n u v ↔ p.length = n

instance SimpleGraph.fintypeSetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.length = n}

Equations

• G.fintypeSetWalkLength u v n = Fintype.ofFinset (G.finsetWalkLength n u v) ⋯

instance SimpleGraph.fintypeSubtypeWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length = n }

Equations

• G.fintypeSubtypeWalkLength u v n = G.fintypeSetWalkLength u v n

theorem SimpleGraph.set_walk_length_toFinset_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u : V) (v : V) : {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v

theorem SimpleGraph.card_set_walk_length_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ℕ) : Fintype.card ↑{p : G.Walk u v | p.length = n} = (G.finsetWalkLength n u v).card

instance SimpleGraph.fintypeSetPathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.IsPath ∧ p.length = n}

Equations

• G.fintypeSetPathLength u v n = Fintype.ofFinset (Finset.filter SimpleGraph.Walk.IsPath (G.finsetWalkLength n u v)) ⋯

theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] (u : V) (v : V) : G.Reachable u v ↔ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n) u v).Nonempty

instance SimpleGraph.instDecidableRelReachable {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : DecidableRel G.Reachable

Equations

• G.instDecidableRelReachable u v = decidable_of_iff' (∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n) u v).Nonempty) ⋯

instance SimpleGraph.instFintypeConnectedComponent {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Fintype G.ConnectedComponent

Equations

• G.instFintypeConnectedComponent = Quotient.fintype G.reachableSetoid

instance SimpleGraph.instDecidablePreconnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Decidable G.Preconnected

Equations

• G.instDecidablePreconnected = inferInstanceAs (Decidable (∀ (u v : V), G.Reachable u v))

instance SimpleGraph.instDecidableConnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Decidable G.Connected

Equations

• G.instDecidableConnected = ⋯.mpr (⋯.mpr inferInstance)

instance SimpleGraph.instDecidableMemSupp {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp)

Equations

• G.instDecidableMemSupp c v = SimpleGraph.ConnectedComponent.recOn c (fun (w : V) => decidable_of_iff (G.Reachable v w) ⋯) ⋯

theorem SimpleGraph.odd_card_iff_odd_components {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Odd (Nat.card V) ↔ Odd (Nat.card ↑{c : G.ConnectedComponent | Odd (Nat.card ↑c.supp)})