ι : Sort ?u.297010
𝕜 : Type ?u.297013
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ Fintype.card ↑(neighborSet G v)
ι : Sort ?u.297010
𝕜 : Type ?u.297013
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ degree G v
rw [← card_neighborSet_eq_degree]
no goals
ι : Sort ?u.297010
𝕜 : Type ?u.297013
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ Fintype.card ↑(neighborSet G v)
exact Set.card_le_of_subset (Set.inter_subset_left _ _)