Theorems · Theorem · sequences and series
Summable.comp_injective
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α]
{f : β → α} [CompleteSpace α] {i : γ → β}, Summable f → Function.Injective i → Summable (f ∘ i)- Cited by
- 22 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- Set.rangeproof · cited by 4,705
- CompleteSpacestatement and proof · cited by 2,532
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- UniformSpacestatement and proof · cited by 2,040
- Summablestatement and proof · cited by 778
- IsUniformAddGroupstatement and proof · cited by 342
- Set.indicator_of_notMemproof · cited by 154
- Summable.indicatorproof · cited by 7
- Function.Injective.summable_iffproof · cited by 3
- Set.indicator_range_compproof · cited by 2
Cited by22
Results whose statement or proof uses this declaration.
- Summable.subtypeproof · cited by 15
- HurwitzKernelBounds.summable_f_natproof · cited by 5
- summable_jacobiTheta₂_term_iffproof · cited by 4
- dist_le_tsum_of_dist_le_of_tendstoproof · cited by 4
- NNReal.summable_comp_injectiveproof · cited by 3
- Summable.sigma_factorproof · cited by 3
- tsum_primes_pow_eqproof · cited by 2
- Summable.norm_lt_oneproof · cited by 2
- EulerProduct.one_sub_inv_eq_geometric_of_summable_normproof · cited by 2
- Summable.prod_factorproof · cited by 2
- summable_cotTermproof · cited by 2
- summable_geometric_two_encodeproof · cited by 2