card_commonNeighbors_le_degree_left

English

For any vertices v,w in G, the number of common neighbors of v and w is at most the degree of v: |commonNeighbors(v,w)| ≤ deg_G(v).

Русский

Для любых вершин v и w графа G число общих соседей v и w не превосходит deg_G(v).

LaTeX

$$$\\#(G.commonNeighbors\) (v,w) \\leq \\deg_G(v)$$$

Lean4

theorem card_commonNeighbors_le_degree_left [DecidableRel G.Adj] (v w : V) :
    Fintype.card (G.commonNeighbors v w) ≤ G.degree v :=
  by
  rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card Set.inter_subset_left

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