op — Mathlib · SciLib

English

Applying MulOpposite on HasSum transports the sum: if HasSum f a L, then HasSum (λa, op(f a)) (op a) L.

Русский

Перенос суммирования через противоположность сохраняет сумму: если HasSum f a L, то HasSum (λa, op(f a)) (op a) L.

LaTeX

$$$\\operatorname{HasSum} f a L \\Rightarrow \\operatorname{HasSum}(\\lambda a, \\operatorname{op}(f a)) (\\operatorname{op} a) L$$$

Lean4

theorem op (hf : HasSum f a L) : HasSum (fun a ↦ op (f a)) (op a) L :=
  (hf.map (@opAddEquiv α _) continuous_op :)

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