Theorems · Theorem · functional analysis
Filter.Tendsto.norm
∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E},
Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖) l (nhds ‖a‖)- Defined in
- Mathlib.Analysis.Normed.Group.Continuity
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 156 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.
Cites8
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 · cited by 5,413
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Tendsto.compproof · cited by 560
- SeminormedAddGroupstatement and proof · cited by 331
- tendsto_normproof · cited by 4
Cited by44
Results whose statement or proof uses this declaration.
- NormedSpace.expSeries_radius_eq_topproof · cited by 27
- ContinuousAt.normproof · cited by 10
- Filter.Tendsto.isBigO_oneproof · cited by 10
- Asymptotics.isBigO_const_of_tendstoproof · cited by 4
- summable_jacobiTheta₂_term_iffproof · cited by 4
- Asymptotics.isBigO_of_div_tendsto_nhdsproof · cited by 3
- Besicovitch.exists_goodδproof · cited by 3
- tendsto_cobounded_of_meromorphicOrderAt_negproof · cited by 3
- Complex.tendsto_mul_log_one_add_of_tendstoproof · cited by 3
- Complex.tendsto_one_add_cpow_exp_of_tendstoproof · cited by 3
- HasProd.normproof · cited by 2
- PhragmenLindelof.right_half_plane_of_tendsto_zero_on_realproof · cited by 2