Theorems · Theorem · general topology
cauchySeq_prod_of_eventually_eq
∀ {E : Type u_2} [inst : SeminormedCommGroup E] {u v : ℕ → E} {N : ℕ},
(∀ n ≥ N, u n = v n) →
(CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), v k) → CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), u k- Defined in
- Mathlib.Analysis.Normed.Group.Uniform
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.prodstatement and proof · cited by 2,356
- le_reflproof · cited by 2,061
- Finset.rangestatement and proof · cited by 1,341
- le_of_ltproof · cited by 1,175
- add_le_addproof · cited by 666
- SeminormedCommGroupstatement and proof · cited by 191
- CauchySeqstatement and proof · cited by 131
- div_mul_cancelproof · cited by 33
- div_self'proof · cited by 25
- Filter.Tendsto.cauchySeqproof · cited by 20
- tendsto_atTop_of_eventually_constproof · cited by 14
- Finset.prod_div_distribproof · cited by 9
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.