Theorems · Theorem · functional analysis
tendsto_zero_iff_norm_tendsto_zero
∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α},
Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun x => ‖f x‖) a (nhds 0)- Defined in
- Mathlib.Analysis.Normed.Group.Continuity
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Norm.normstatement and proof · cited by 5,413
- Filter.Tendstostatement and proof · cited by 3,814
- add_zeroproof · cited by 2,707
- SeminormedAddGroupstatement and proof · cited by 331
- norm_negproof · cited by 190
- tendsto_iff_norm_neg_add_tendsto_zeroproof · cited by 1
Cited by29
Results whose statement or proof uses this declaration.
- squeeze_zero_norm'proof · cited by 4
- NormedRing.inverse_continuousAtproof · cited by 3
- Function.Periodic.qParam_tendstoproof · cited by 3
- tendsto_pow_atTop_nhds_zero_iff_norm_lt_oneproof · cited by 3
- PadicInt.hasSum_mahlerSeriesproof · cited by 2
- hasFDerivAt_of_tendstoUniformlyOnFilterproof · cited by 2
- Complex.continuousAt_cpow_zero_of_re_posproof · cited by 2
- CuspFormClass.petersson_bounded_leftproof · cited by 2
- contDiff_norm_rpowproof · cited by 2
- tendsto_pow_const_mul_const_pow_of_abs_lt_oneproof · cited by 2
- UpperHalfPlane.IsZeroAtImInfty.slashproof · cited by 1
- taylor_tendstoproof · cited by 1