walkLengthTwoEquivCommonNeighbors

English

There is a natural bijection between length-two walks from u to v and the common neighbors of u and v.

Русский

Существует естественная биекция между ходами длины два от u к v и общими соседями u и v.

LaTeX

$${ p : G.Walk u v // p.length = 2 } ≃ G.commonNeighbors u v$$

Lean4

/-- 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. -/
@[simps]
def walkLengthTwoEquivCommonNeighbors (u v : V) : { p : G.Walk u v // p.length = 2 } ≃ G.commonNeighbors u v
    where
  toFun
    p :=
    ⟨p.val.snd,
      match p with
      | ⟨.cons _ (.cons _ .nil), _⟩ => ⟨‹G.Adj u _›, ‹G.Adj _ v›.symm⟩⟩
  invFun w := ⟨w.prop.1.toWalk.concat w.prop.2.symm, rfl⟩
  left_inv
    | ⟨.cons _ (.cons _ .nil), hp⟩ => by rfl

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