intro iM
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ (Balanced M.t fun i => card (MultiPart.P M i)) → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)