ι : Sort ?u.287178
𝕜 : Type ?u.287181
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
v : V
⊢ card ∅ = 0
ι : Sort ?u.287178
𝕜 : Type ?u.287181
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
v : V
⊢ degree ⊥ v = 0
erw [degree, neighborFinset_eq_filter, filter_False]
no goals
ι : Sort ?u.287178
𝕜 : Type ?u.287181
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
v : V
⊢ card ∅ = 0
exact Finset.card_empty