no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card s) * 0 ≤ ↑(card ∅)
simp
no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card t) * 0 ≤ ↑(card ∅)
simp