unfold degOn
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card