no goals
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (interedges r s t) = ∑ b in P.parts, card (interedges r s b)
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (Finset.biUnion P.parts fun b => interedges r s b) = ∑ b in P.parts, card (interedges r s b)
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (interedges r s t) = ∑ b in P.parts, card (interedges r s b)
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ ∀ (x : Finset β), x ∈ P.parts → ∀ (y : Finset β), y ∈ P.parts → x ≠ y → Disjoint (interedges r s x) (interedges r s y)
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (Finset.biUnion P.parts fun b => interedges r s b) = ∑ b in P.parts, card (interedges r s b)
rw [card_biUnion]
no goals
𝕜 : Type ?u.24112
ι : Type ?u.24115
κ : Type ?u.24118
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ ∀ (x : Finset β), x ∈ P.parts → ∀ (y : Finset β), y ∈ P.parts → x ≠ y → Disjoint (interedges r s x) (interedges r s y)
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)