English
If vertices v and w are adjacent, then the number of common neighbors of v and w is strictly less than deg_G(v).
Русский
Если вершины v и w соседствуют, то число общих соседей v и w строго меньше deg_G(v).
LaTeX
$$$G.Adj(v,w)\\ \\Rightarrow\\ #(G.commonNeighbors(v,w)) < \\deg_G(v)$$$
Lean4
/-- If the condition `G.Adj v w` fails, then `card_commonNeighbors_le_degree` is
the best we can do in general. -/
theorem card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.Adj] {v w : V} (h : G.Adj v w) :
Fintype.card (G.commonNeighbors v w) < G.degree v := by
classical
rw [← Set.toFinset_card]
apply Finset.card_lt_card
rw [Finset.ssubset_iff]
use w
constructor
· rw [Set.mem_toFinset]
apply notMem_commonNeighbors_right
· rw [Finset.insert_subset_iff]
constructor
· simpa
· rw [neighborFinset, Set.toFinset_subset_toFinset]
exact G.commonNeighbors_subset_neighborSet_left _ _
