Theorems · Theorem · functional analysis
cauchySeq_finset_of_norm_bounded
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ},
Summable g → (∀ (i : ι), ‖f i‖ ≤ g i) → CauchySeq fun s => ∑ i ∈ s, f i- Cited by
- 6 results in Mathlib
- Foundations
- Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finsetstatement · cited by 13,712
- Norm.normstatement and proof · cited by 5,413
- Finset.sumstatement · cited by 5,195
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Summablestatement and proof · cited by 778
- Filter.Eventually.of_forallproof · cited by 526
- CauchySeqstatement · cited by 131
- cauchySeq_finset_of_norm_bounded_eventuallyproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- Summable.of_norm_boundedproof · cited by 25
- HasFPowerSeriesWithinAt.compproof · cited by 2
- HasFPowerSeriesAt.eventually_hasSum_of_compproof · cited by 1
- HasFPowerSeriesAt.tendsto_partialSum_prod_of_compproof · cited by 1
- cauchySeq_finset_of_geometric_boundproof · cited by 1
- cauchySeq_finset_of_summable_normproof · cited by 1