no goals
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ card (interedges r s t) = ∑ a in P.parts, card (interedges r a t)
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id.def]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ card (Finset.biUnion P.parts fun a => interedges r a t) = ∑ a in P.parts, card (interedges r a t)
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ card (interedges r s t) = ∑ a in P.parts, card (interedges r a t)
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id.def]
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ ∀ (x : Finset α), x ∈ P.parts → ∀ (y : Finset α), y ∈ P.parts → x ≠ y → Disjoint (interedges r x t) (interedges r y t)
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ card (Finset.biUnion P.parts fun a => interedges r a t) = ∑ a in P.parts, card (interedges r a t)
rw [card_biUnion]
no goals
𝕜 : Type ?u.21732
ι : Type ?u.21735
κ : Type ?u.21738
α : 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 α
P : Finpartition s
t : Finset β
⊢ ∀ (x : Finset α), x ∈ P.parts → ∀ (y : Finset α), y ∈ P.parts → x ≠ y → Disjoint (interedges r x t) (interedges r y t)
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _