Structures · Analysis
Norm
Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds norm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by14
Concrete types that are instances28
- Real
- Quiver.Hom
- Complex
- SeparationQuotient
- ContinuousLinearMap
- BoundedContinuousFunction
- Padic
- CStarMatrix
- UniformSpace.Completion
- PadicInt
- WithLp
- ContinuousMapZero
- PiTensorProduct
- NumberField.InfiniteAdeleRing
- WithCStarModule
- ContinuousMultilinearMap
- Hamming
- ContinuousAffineMap
- PiLp
- NormedAddGroupHom
- Subtype
- Prod
- OrderDual
- ULift
- HasQuotient.Quotient
- ContinuousMap
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by465
- Norm.norm
- Asymptotics.IsBigO
- Asymptotics.IsLittleO
- norm_smul
- Asymptotics.IsBigOWith
- norm_mul
- Asymptotics.IsTheta
- Asymptotics.IsBigO.trans
- Asymptotics.isBigO_refl
- Asymptotics.IsBigOWith_def
- Asymptotics.IsBigOWith.isBigO
- Asymptotics.IsLittleO.isBigO
- Asymptotics.IsBigO.comp_tendsto
- Asymptotics.IsBigO.trans_isLittleO
- UpperHalfPlane.IsBoundedAtImInfty
- Asymptotics.IsBigO_def
- Asymptotics.isLittleO_iff
- Asymptotics.IsBigO.isBigOWith
- Asymptotics.IsBigO.add
- Asymptotics.IsLittleO.congr'
- Asymptotics.isLittleO_one_iff
- Asymptotics.IsLittleO.trans_isBigO
- Asymptotics.IsBigO.exists_pos
- Asymptotics.IsLittleO_def
- Asymptotics.isBigO_iff
- Asymptotics.IsLittleO.comp_tendsto
- Asymptotics.IsLittleO.add
- Asymptotics.IsBigOWith.bound
- Asymptotics.IsBigO.const_mul_left
- Asymptotics.IsBigOWith.of_bound
- Asymptotics.IsBigO.congr'
- Asymptotics.IsBigO.mono
- Asymptotics.IsBigO.of_bound
- Asymptotics.IsBigO.norm_left
- Filter.BoundedAtFilter
- Asymptotics.IsBigOWith.congr_const
- Asymptotics.IsBigOWith.trans
- Asymptotics.IsLittleO.of_isBigOWith
- Asymptotics.IsLittleO.congr_left
- Asymptotics.isBigO_of_le
- Asymptotics.isTheta_refl
- Asymptotics.IsTheta.symm
- Asymptotics.IsBigO.of_norm_eventuallyLE
- Asymptotics.isBigO_norm_left
- Filter.Tendsto.isBigO_one
- CStarModule.innerₛₗ
- Asymptotics.IsLittleO.forall_isBigOWith
- Asymptotics.IsBigO.exists_nonneg
- Asymptotics.IsBigO.sub
- Asymptotics.IsLittleO.neg_left
Ancestors0
No ancestors.