no goals
𝕜 : Type ?u.20604
ι : Type ?u.20607
κ : Type ?u.20610
α : Type u_2
β : Type u_1
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
t : Finset β
⊢ edgeDensity r ∅ t = 0
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]