Theorems · Theorem · general topology
norm_map
∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖- Defined in
- Mathlib.Analysis.Normed.Group.Uniform
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- FunLikestatement and proof · cited by 2,560
- map_zeroproof · cited by 1,614
- SeminormedAddGroupstatement and proof · cited by 331
- ZeroHomClassstatement and proof · cited by 74
- IsometryClassstatement and proof · cited by 19
- Isometry.norm_map_of_map_zeroproof · cited by 13
- IsometryClass.isometryproof · cited by 12
Cited by20
Results whose statement or proof uses this declaration.
- LinearIsometryEquiv.norm_mapproof · cited by 39
- LinearIsometry.norm_toContinuousLinearMapproof · cited by 13
- LinearIsometry.norm_mapproof · cited by 12
- nnnorm_mapproof · cited by 5
- LinearIsometry.norm_toContinuousLinearMap_leproof · cited by 5
- Function.HasTemperateGrowth.of_fderivproof · cited by 4
- GaussianFourier.integral_cexp_neg_mul_sq_norm_addproof · cited by 2
- hasSum_sq_fourierCoeffproof · cited by 2
- not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filterproof · cited by 2
- RKHS.norm_kernel_leproof · cited by 1
- FormalMultilinearSeries.radius_le_radius_derivSeriesproof · cited by 1
- UpperHalfPlane.qExpansionFormalMultilinearSeries_apply_normproof · cited by 1