intro h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
⊢ card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α) → TuranPartition M
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
⊢ TuranPartition M