unop — Mathlib

English

Applying unop to HasSum preserves the summed value: HasSum f a L implies HasSum (unop ∘ f) (unop a) L.

Русский

Применение unop к HasSum сохраняет сумму: HasSum f a L → HasSum (unop ∘ f) (unop a) L.

LaTeX

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

Lean4

theorem unop {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a L) : HasSum (fun a ↦ unop (f a)) (unop a) L :=
  (hf.map (@opAddEquiv α _).symm continuous_unop :)

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