no goals
ι : Sort ?u.269926
𝕜 : Type ?u.269929
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 ↑(neighborSet G v)
inst✝¹ : Fintype ↑(neighborSet (Gᶜ) v)
inst✝ : Fintype V
⊢ degree (Gᶜ) v = Fintype.card V - 1 - degree G v
classical
  rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
  simp [card_disjoint_union (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
ι : Sort ?u.269926
𝕜 : Type ?u.269929
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 ↑(neighborSet G v)
inst✝¹ : Fintype ↑(neighborSet (Gᶜ) v)
inst✝ : Fintype V
⊢ degree (Gᶜ) v = card (Set.toFinset (neighborSet G v) ∪ Set.toFinset (neighborSet (Gᶜ) v)) - degree G v
ι : Sort ?u.269926
𝕜 : Type ?u.269929
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 ↑(neighborSet G v)
inst✝¹ : Fintype ↑(neighborSet (Gᶜ) v)
inst✝ : Fintype V
⊢ degree (Gᶜ) v = Fintype.card V - 1 - degree G v
rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
no goals
ι : Sort ?u.269926
𝕜 : Type ?u.269929
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 ↑(neighborSet G v)
inst✝¹ : Fintype ↑(neighborSet (Gᶜ) v)
inst✝ : Fintype V
⊢ degree (Gᶜ) v = card (Set.toFinset (neighborSet G v) ∪ Set.toFinset (neighborSet (Gᶜ) v)) - degree G v
simp [card_disjoint_union (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]