V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
haveI := Classical.decEq V
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ card univ = ∑ x : V, card (filter (fun d => d.fst = x) univ)
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
no goals
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ card univ = ∑ x : V, card (filter (fun d => d.fst = x) univ)
exact card_eq_sum_card_fiberwise (by simp)
no goals
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ ∀ (x : Dart G), x ∈ univ → x.fst ∈ univ
simp