𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a in P.parts, card (interedges r a t) = ∑ x in P.parts, ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ card (interedges r s t) = ∑ ab in P.parts ×ˢ Q.parts, card (interedges r ab.fst ab.snd)
rw [card_interedges_finpartition_left _ P, sum_product]
case e_f
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a => card (interedges r a t)) = fun x => ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a in P.parts, card (interedges r a t) = ∑ x in P.parts, ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
congr
case e_f.h
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ card (interedges r x✝ t) = ∑ y in Q.parts, card (interedges r (x✝, y).fst (x✝, y).snd)
case e_f
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a => card (interedges r a t)) = fun x => ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
ext
no goals
case e_f.h
𝕜 : Type ?u.26491
ι : Type ?u.26494
κ : Type ?u.26497
α : 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 : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ card (interedges r x✝ t) = ∑ y in Q.parts, card (interedges r (x✝, y).fst (x✝, y).snd)
rw [card_interedges_finpartition_right]