𝕜 : Type ?u.18447
ι : Type ?u.18450
κ : Type ?u.18453
α : 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 : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card (interedges r s t)) + ↑(card (interedges (fun x y => ¬r x y) s t)) = ↑(card s) * ↑(card t)

𝕜 : Type ?u.18447
ι : Type ?u.18450
κ : Type ?u.18453
α : 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 : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card s) * ↑(card t) ≠ 0
𝕜 : Type ?u.18447
ι : Type ?u.18450
κ : Type ?u.18453
α : 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 : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ edgeDensity r s t + edgeDensity (fun x y => ¬r x y) s t = 1
rw [edgeDensity, edgeDensity, div_add_div_same, div_eq_one_iff_eq]
no goals
𝕜 : Type ?u.18447
ι : Type ?u.18450
κ : Type ?u.18453
α : 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 : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card (interedges r s t)) + ↑(card (interedges (fun x y => ¬r x y) s t)) = ↑(card s) * ↑(card t)
exact_mod_cast card_interedges_add_card_interedges_compl r s t
no goals
𝕜 : Type ?u.18447
ι : Type ?u.18450
κ : Type ?u.18453
α : 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 : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card s) * ↑(card t) ≠ 0
exact_mod_cast (mul_pos hs.card_pos ht.card_pos).ne'