α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(card A * (card A - 1)) * ε
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ IsUniform ⊥ G ε
rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty,
  Nat.cast_zero]
no goals
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(card A * (card A - 1)) * ε
exact mul_nonneg (Nat.cast_nonneg _) hε.le