card_commonNeighbors_lt_card_verts

English

For any vertices v,w, the number of common neighbors is strictly less than the total number of vertices: |commonNeighbors(v,w)| < |V|.

Русский

Для любых вершин v и w число общих соседей строго меньше числа вершин: |commonNeighbors(v,w)| < |V|.

LaTeX

$$$\\#(G.commonNeighbors\\) (v,w) < \\lvert V \\rvert$$$

Lean4

theorem card_commonNeighbors_lt_card_verts [DecidableRel G.Adj] (v w : V) :
    Fintype.card (G.commonNeighbors v w) < Fintype.card V :=
  Nat.lt_of_le_of_lt (G.card_commonNeighbors_le_degree_left _ _) (G.degree_lt_card_verts v)

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