case h
𝕜 : Type ?u.16981
ι : Type ?u.16984
κ : Type ?u.16987
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ ↑(card (interedges r s t)) ≤ ↑(card s) * ↑(card t)

case hb
𝕜 : Type ?u.16981
ι : Type ?u.16984
κ : Type ?u.16987
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(card s) * ↑(card t)
𝕜 : Type ?u.16981
ι : Type ?u.16984
κ : Type ?u.16987
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ edgeDensity r s t ≤ 1
apply div_le_one_of_le
no goals
case h
𝕜 : Type ?u.16981
ι : Type ?u.16984
κ : Type ?u.16987
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ ↑(card (interedges r s t)) ≤ ↑(card s) * ↑(card t)
exact_mod_cast card_interedges_le_mul r s t
no goals
case hb
𝕜 : Type ?u.16981
ι : Type ?u.16984
κ : Type ?u.16987
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(card s) * ↑(card t)
exact_mod_cast Nat.zero_le _