monlib / preq.finset - mathlib3 docs

@[simp]

theorem finset.sum_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} [add_comm_monoid β] {s : finset α} {t : finset γ} {u : finset ζ} {f : α → γ → ζ → β} :

s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), f x y z))) = u.sum (λ (z : ζ), s.sum (λ (x : α), t.sum (λ (y : γ), f x y z)))

source

@[simp]

theorem finset.sum_3_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} [add_comm_monoid β] {s : finset α} {t : finset γ} {u : finset ζ} {f : α → γ → ζ → β} :

s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), f x y z))) = u.sum (λ (z : ζ), t.sum (λ (y : γ), s.sum (λ (x : α), f x y z)))

source

@[simp]

theorem finset.sum_4_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [add_comm_monoid β] {s : finset α} {t : finset γ} {u : finset ζ} {v : finset ε} {f : α → γ → ζ → ε → β} :

s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), v.sum (λ (w : ε), f x y z w)))) = v.sum (λ (w : ε), s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), f x y z w))))

source

@[simp]

theorem finset.sum_sum_comm_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [add_comm_monoid β] {s : finset α} {t : finset γ} {u : finset ζ} {v : finset ε} {f : α → γ → ζ → ε → β} :

s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), v.sum (λ (w : ε), f x y z w)))) = s.sum (λ (x : α), t.sum (λ (y : γ), v.sum (λ (w : ε), u.sum (λ (z : ζ), f x y z w))))

source

@[simp]

theorem finset.sum_sum_sum {β : Type u_1} {α : Type u_2} {γ : Type u_3} {ζ : Type u_4} [add_comm_monoid β] {s : finset γ} {t : finset α} {g : finset ζ} {f : γ → α → ζ → β} :

s.sum (λ (x : γ), t.sum (λ (y : α), g.sum (λ (z : ζ), f x y z))) = g.sum (λ (z : ζ), s.sum (λ (x : γ), t.sum (λ (y : α), f x y z)))

source

theorem finset.sum_4_swap_2 {β : Type u_1} {α : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [add_comm_monoid β] {s : finset γ} {t : finset α} {u : finset ζ} {v : finset ε} {f : γ → α → ζ → ε → β} :

s.sum (λ (x : γ), t.sum (λ (y : α), u.sum (λ (z : ζ), v.sum (λ (w : ε), f x y z w)))) = u.sum (λ (z : ζ), v.sum (λ (w : ε), s.sum (λ (x : γ), t.sum (λ (y : α), f x y z w))))

source

theorem finset.sum_5_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} {κ : Type u_6} [add_comm_monoid β] {s : finset α} {t : finset γ} {u : finset ζ} {v : finset ε} {k : finset κ} {f : α → γ → ζ → ε → κ → β} :

s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), v.sum (λ (w : ε), k.sum (λ (vz : κ), f x y z w vz))))) = k.sum (λ (vz : κ), s.sum (λ (x : α), t.sum (λ (y : γ), u.sum (λ (z : ζ), v.sum (λ (w : ε), f x y z w vz)))))

source

@[simp]

theorem forall.rotate {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → β → γ → Prop} :

(∀ (x : α) (y : β) (z : γ), p x y z) ↔ ∀ (z : γ) (x : α) (y : β), p x y z

source

@[simp]

theorem forall_forall_comm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {ζ : Sort u_4} {p : α → β → γ → ζ → Prop} :

(∀ (x : α) (y : β) (z : γ) (w : ζ), p x y z w) ↔ ∀ (x : α) (z : γ) (y : β) (w : ζ), p x y z w

mathlib3 documentation

finset #