# Topological sums and functorial constructions #

Lemmas on the interaction of `tprod`, `tsum`, `HasProd`, `HasSum` etc. with products, Sigma and Pi types, `MulOpposite`, etc.

## Product, Sigma and Pi types #

source
theorem hasProd_pi_single {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
HasProd (Pi.mulSingle b a) a
source
theorem hasSum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
HasSum (Pi.single b a) a
source
@[simp]
theorem tprod_pi_single {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
∏' (b' : β), Pi.mulSingle b a b' = a
source
@[simp]
theorem tsum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
∑' (b' : β), Pi.single b a b' = a
source
theorem tprod_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (b : β) (t : Set γ) (f : β × γ → α) :
∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)
source
theorem tsum_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (b : β) (t : Set γ) (f : β × γ → α) :
∑' (x : ↑({b} ×ˢ t)), f ↑x = ∑' (c : ↑t), f (b, ↑c)
source
theorem tprod_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (s : Set β) (c : γ) (f : β × γ → α) :
∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)
source
theorem tsum_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (c : γ) (f : β × γ → α) :
∑' (x : ↑(s ×ˢ {c})), f ↑x = ∑' (b : ↑s), f (↑b, c)
source
theorem Multipliable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β × γ → α} (hf : Multipliable f) :
Multipliable fun (p : γ × β) => f p.swap
source
theorem Summable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β × γ → α} (hf : Summable f) :
Summable fun (p : γ × β) => f p.swap
source
theorem HasProd.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {L : SummationFilter β} [CommMonoid α] [TopologicalSpace α] [CommMonoid γ] [TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a L) (hg : HasProd g b L) :
HasProd (fun (x : β) => (f x, g x)) (a, b) L
source
theorem HasSum.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [AddCommMonoid γ] [TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasSum f a L) (hg : HasSum g b L) :
HasSum (fun (x : β) => (f x, g x)) (a, b) L
source
theorem HasProd.sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : α ⊕ β → M} {a b : M} (h₁ : HasProd (f ∘ Sum.inl) a) (h₂ : HasProd (f ∘ Sum.inr) b) :
HasProd f (a * b)
source
theorem HasSum.sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : α ⊕ β → M} {a b : M} (h₁ : HasSum (f ∘ Sum.inl) a) (h₂ : HasSum (f ∘ Sum.inr) b) :
HasSum f (a + b)
source
theorem Multipliable.tprod_sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : α ⊕ β → M} (h₁ : Multipliable (f ∘ Sum.inl)) (h₂ : Multipliable (f ∘ Sum.inr)) :
∏' (i : α ⊕ β), f i = (∏' (i : α), f (Sum.inl i)) * ∏' (i : β), f (Sum.inr i)
source
theorem Summable.tsum_sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : α ⊕ β → M} (h₁ : Summable (f ∘ Sum.inl)) (h₂ : Summable (f ∘ Sum.inr)) :
∑' (i : α ⊕ β), f i = ∑' (i : α), f (Sum.inl i) + ∑' (i : β), f (Sum.inr i)

For the statement that `tsum` commutes with `Finset.sum`, see `Summable.tsum_finsetSum`.

source
theorem Multipliable.sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (f : α ⊕ β → M) (h₁ : Multipliable (f ∘ Sum.inl)) (h₂ : Multipliable (f ∘ Sum.inr)) :
Multipliable f
source
theorem Summable.sum {α : Type u_4} {β : Type u_5} {M : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : α ⊕ β → M) (h₁ : Summable (f ∘ Sum.inl)) (h₂ : Summable (f ∘ Sum.inr)) :
Summable f
source
theorem HasProd.sigma {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasProd f a) (hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b)) :
HasProd g a
source
theorem HasSum.sigma {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b)) :
HasSum g a
source
theorem HasProd.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a) (hf : ∀ (b : β), HasProd (fun (c : γ) => f (b, c)) (g b)) :
HasProd g a

If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to `{b} × γ` has product `g b`, then the function `g` has product `a`.

source
theorem HasSum.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ) => f (b, c)) (g b)) :
HasSum g a

If a series `f` on `β × γ` has sum `a` and for each `b` the restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`.

source
theorem Multipliable.sigma' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Multipliable f) (hf : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩) :
Multipliable fun (b : β) => ∏' (c : γ b), f ⟨b, c⟩
source
theorem Summable.sigma' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Summable f) (hf : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩) :
Summable fun (b : β) => ∑' (c : γ b), f ⟨b, c⟩
source
theorem HasProd.sigma_of_hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasProd g a) (hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b)) (hf' : Multipliable f) :
HasProd f a
source
theorem HasSum.sigma_of_hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasSum g a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b)) (hf' : Summable f) :
HasSum f a
source
theorem Multipliable.tprod_sigma' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (h₁ : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩) (h₂ : Multipliable f) :
∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
source
theorem Summable.tsum_sigma' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (h₁ : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩) (h₂ : Summable f) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
source
theorem Multipliable.tprod_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {f : β × γ → α} (h : Multipliable f) (h₁ : ∀ (b : β), Multipliable fun (c : γ) => f (b, c)) :
∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
source
theorem Summable.tsum_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {f : β × γ → α} (h : Summable f) (h₁ : ∀ (b : β), Summable fun (c : γ) => f (b, c)) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
source
theorem Multipliable.tprod_prod_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {f : β → γ → α} (h : Multipliable (Function.uncurry f)) (h₁ : ∀ (b : β), Multipliable fun (c : γ) => f b c) :
∏' (p : β × γ), Function.uncurry f p = ∏' (b : β) (c : γ), f b c
source
theorem Summable.tsum_prod_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {f : β → γ → α} (h : Summable (Function.uncurry f)) (h₁ : ∀ (b : β), Summable fun (c : γ) => f b c) :
∑' (p : β × γ), Function.uncurry f p = ∑' (b : β) (c : γ), f b c
source
theorem Multipliable.tprod_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {f : β → γ → α} (h : Multipliable (Function.uncurry f)) (h₁ : ∀ (b : β), Multipliable (f b)) (h₂ : ∀ (c : γ), Multipliable fun (b : β) => f b c) :
∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
source
theorem Summable.tsum_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {f : β → γ → α} (h : Summable (Function.uncurry f)) (h₁ : ∀ (b : β), Summable (f b)) (h₂ : ∀ (c : γ), Summable fun (b : β) => f b c) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
source
theorem HasProd.of_sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b)) (hg : HasProd g a) (h : CauchySeq fun (s : Finset ((b : β) × γ b)) => ∏ i ∈ s, f i) :
HasProd f a
source
theorem HasSum.of_sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α} (hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b)) (hg : HasSum g a) (h : CauchySeq fun (s : Finset ((b : β) × γ b)) => ∑ i ∈ s, f i) :
HasSum f a
source
theorem Multipliable.sigma_factor {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Multipliable f) (b : β) :
Multipliable fun (c : γ b) => f ⟨b, c⟩
source
theorem Summable.sigma_factor {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Summable f) (b : β) :
Summable fun (c : γ b) => f ⟨b, c⟩
source
theorem Multipliable.sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Multipliable f) :
Multipliable fun (b : β) => ∏' (c : γ b), f ⟨b, c⟩
source
theorem Summable.sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Summable f) :
Summable fun (b : β) => ∑' (c : γ b), f ⟨b, c⟩
source
theorem Multipliable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {f : β × γ → α} (h : Multipliable f) (b : β) :
Multipliable fun (c : γ) => f (b, c)
source
theorem Summable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : β × γ → α} (h : Summable f) (b : β) :
Summable fun (c : γ) => f (b, c)
source
theorem Multipliable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {f : β × γ → α} (h : Multipliable f) :
Multipliable fun (b : β) => ∏' (c : γ), f (b, c)
source
theorem Summable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : β × γ → α} (h : Summable f) :
Summable fun (b : β) => ∑' (c : γ), f (b, c)
source
theorem HasProd.tprod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) :
HasProd (fun (c : γ) => ∏' (b : ↑(g ⁻¹' {c})), f ↑b) a
source
theorem HasSum.tsum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} {a : α} (hf : HasSum f a) (g : β → γ) :
HasSum (fun (c : γ) => ∑' (b : ↑(g ⁻¹' {c})), f ↑b) a
source
theorem Multipliable.tprod_sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Multipliable f) :
∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
source
theorem Summable.tsum_sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α} (ha : Summable f) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
source
theorem Multipliable.tprod_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α] {f : β × γ → α} (h : Multipliable f) :
∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
source
theorem Summable.tsum_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : β × γ → α} (h : Summable f) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
source
theorem Multipliable.tprod_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α] {f : β → γ → α} (h : Multipliable (Function.uncurry f)) :
∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
source
theorem Summable.tsum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : β → γ → α} (h : Summable (Function.uncurry f)) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
source
theorem Pi.hasProd {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → CommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} {g : (x : α) → X x} :
HasProd f g L ↔ ∀ (x : α), HasProd (fun (i : ι) => f i x) (g x) L
source
theorem Pi.hasSum {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → AddCommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} {g : (x : α) → X x} :
HasSum f g L ↔ ∀ (x : α), HasSum (fun (i : ι) => f i x) (g x) L
source
theorem Pi.multipliable {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → CommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} :
Multipliable f L ↔ ∀ (x : α), Multipliable (fun (i : ι) => f i x) L
source
theorem Pi.summable {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → AddCommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} :
Summable f L ↔ ∀ (x : α), Summable (fun (i : ι) => f i x) L
source
theorem tprod_apply {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → CommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} [L.NeBot] [∀ (x : α), T2Space (X x)] {f : ι → (x : α) → X x} {x : α} (hf : Multipliable f L) :
(∏'[L] (i : ι), f i) x = ∏'[L] (i : ι), f i x
source
theorem tsum_apply {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [(x : α) → AddCommMonoid (X x)] [(x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} [L.NeBot] [∀ (x : α), T2Space (X x)] {f : ι → (x : α) → X x} {x : α} (hf : Summable f L) :
(∑'[L] (i : ι), f i) x = ∑'[L] (i : ι), f i x

## Multiplicative opposite #

source
theorem HasSum.op {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (hf : HasSum f a L) :
HasSum (fun (a : β) => MulOpposite.op (f a)) (MulOpposite.op a) L
source
theorem Summable.op {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (hf : Summable f L) :
Summable (MulOpposite.op ∘ f) L
source
theorem HasSum.unop {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α ᵐᵒᵖ} {a : α ᵐᵒᵖ} (hf : HasSum f a L) :
HasSum (fun (a : β) => MulOpposite.unop (f a)) (MulOpposite.unop a) L
source
theorem Summable.unop {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α ᵐᵒᵖ} (hf : Summable f L) :
Summable (MulOpposite.unop ∘ f) L
source
@[simp]
theorem hasSum_op {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} :
HasSum (fun (a : β) => MulOpposite.op (f a)) (MulOpposite.op a) L ↔ HasSum f a L
source
@[simp]
theorem hasSum_unop {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α ᵐᵒᵖ} {a : α ᵐᵒᵖ} :
HasSum (fun (a : β) => MulOpposite.unop (f a)) (MulOpposite.unop a) L ↔ HasSum f a L
source
@[simp]
theorem summable_op {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} :
Summable (fun (a : β) => MulOpposite.op (f a)) L ↔ Summable f L
source
theorem summable_unop {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α ᵐᵒᵖ} :
Summable (fun (a : β) => MulOpposite.unop (f a)) L ↔ Summable f L
source
theorem tsum_op {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] :
∑'[L] (x : β), MulOpposite.op (f x) = MulOpposite.op (∑'[L] (x : β), f x)
source
theorem tsum_unop {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : β → α ᵐᵒᵖ} :
∑'[L] (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑'[L] (x : β), f x)

## Interaction with the star #

source
theorem HasSum.star {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} {a : α} (h : HasSum f a L) :
HasSum (fun (b : β) => Star.star (f b)) (Star.star a) L
source
theorem Summable.star {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} (hf : Summable f L) :
Summable (fun (b : β) => Star.star (f b)) L
source
theorem Summable.ofStar {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} (hf : Summable (fun (b : β) => Star.star (f b)) L) :
Summable f L
source
@[simp]
theorem summable_star_iff {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} :
Summable (fun (b : β) => star (f b)) L ↔ Summable f L
source
@[simp]
theorem summable_star_iff' {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} :
Summable (star f) L ↔ Summable f L
source
theorem tsum_star {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} [T2Space α] :
star (∑'[L] (b : β), f b) = ∑'[L] (b : β), star (f b)