ι : Sort ?u.279944
𝕜 : Type ?u.279947
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✝³ : LocallyFinite G✝
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : IsRegularOfDegree G k
v : V
⊢ degree (Gᶜ) v = Fintype.card V - 1 - k
ι : Sort ?u.279944
𝕜 : Type ?u.279947
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✝³ : LocallyFinite G✝
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : IsRegularOfDegree G k
⊢ IsRegularOfDegree (Gᶜ) (Fintype.card V - 1 - k)
intro v
no goals
ι : Sort ?u.279944
𝕜 : Type ?u.279947
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✝³ : LocallyFinite G✝
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : IsRegularOfDegree G k
v : V
⊢ degree (Gᶜ) v = Fintype.card V - 1 - k
rw [degree_compl, h v]