V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ v ≠ w
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ Fintype.card ↑(commonNeighbors ⊤ v w) = Fintype.card V - 2
rw [card_commonNeighbors_top]
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ v ≠ w
exact h