no goals
𝕜 : Type ?u.3694
ι : Type ?u.3697
κ : Type ?u.3700
α : 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 (interedges (fun x y => ¬r x y) s t) = card s * card t
classical
rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
𝕜 : Type ?u.3694
ι : Type ?u.3697
κ : Type ?u.3700
α : 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 β
⊢ Disjoint (filter (fun e => r e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬r e.fst e.snd) (s ×ˢ t))
𝕜 : Type ?u.3694
ι : Type ?u.3697
κ : Type ?u.3700
α : 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 (interedges (fun x y => ¬r x y) s t) = card s * card t
rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
no goals
𝕜 : Type ?u.3694
ι : Type ?u.3697
κ : Type ?u.3700
α : 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 β
⊢ Disjoint (filter (fun e => r e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬r e.fst e.snd) (s ×ˢ t))
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2