prod_symm — Mathlib

English

If f is Multipliable on β × γ, then the function p ↦ f(p.swap) is Multipliable on γ × β. This expresses the symmetry of the two-factor indexing.

Русский

Если f объявлена на β × γ и сходится, то f(p.swap) сходится на γ × β, то есть симметрия двойного индекса.

LaTeX

$$$\\forall {f},\\ Multipliable f \\Rightarrow Multipliable (p \\mapsto f(p.swap))$$$

Lean4

@[to_additive Summable.prod_symm]
theorem prod_symm {f : β × γ → α} (hf : Multipliable f) : Multipliable fun p : γ × β ↦ f p.swap :=
  (Equiv.prodComm γ β).multipliable_iff.2 hf

Похожие утверждения