Structures · Analysis
NormedAddGroup
A normed group is an additive group endowed with a norm for which dist x y = ‖-x + y‖ defines
a metric space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds dist_eq
Extends3
Extended by1
Forgetful instances
Concrete types that are instances7
- Hamming
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- norm_pos_iff
- norm_ne_zero_iff
- norm_eq_zero
- norm_le_zero_iff
- eq_zero_or_norm_pos
- nnnorm_ne_zero_iff
- nnnorm_eq_zero
- HasCompactSupport.norm
- norm_sub_eq_zero_iff
- ProbabilityTheory.IndepFun.integrable_left_of_integrable_op
- Continuous.bounded_above_of_compact_support
- ProbabilityTheory.IndepFun.integrable_right_of_integrable_op
- norm_sub_pos_iff
- tendsto_norm_nhdsNE_zero
- eq_zero_or_nnnorm_pos
- MeasureTheory.HasFiniteIntegral.smul_enorm
- tendsto_norm_neg_add_self_nhdsNE
- ContinuousOn.isBigO_rev_principal
- hasCompactSupport_norm_iff
- ContinuousOn.isBigOWith_rev_principal
- comap_norm_nhdsGT_zero
- nnnorm_pos
- HasCompactSupport.exists_pos_le_norm
- ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul
- NormedAddGroup.dist_eq
- AddSubgroupClass.normedAddGroup
- NormedAddGroup.toAddGroup
- NormedAddGroup.toENormedAddMonoid
- OrderDual.normedAddGroup
- Multiplicative.normedGroup
- MulOpposite.instNormedAddGroup
- eq_of_norm_sub_le_zero
- Pi.normedAddGroup
- eq_of_norm_sub_eq_zero
- NormedAddGroup.induced
- NormedAddGroup.toNorm
- NormedAddCommGroup.induced
- NormedAddGroup.toMetricSpace
- HasCompactMulSupport.exists_pos_le_norm
- ContinuousOn.isTheta_principal
- ULift.normedAddGroup
- ProbabilityTheory.IndepFun.integrable_right_of_integrable_mul
- normAddGroupNorm
- NormedAddGroup.toSeminormedAddGroup
- AddSubgroup.normedAddGroup
- Prod.normedAddGroup
Ancestors57
- Add
- AddAction
- AddCancelMonoid
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- EDist
- EMetricSpace
- ENorm
- HAdd
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- LocallyPathConnectedSpace
- MetricSpace
- NNDist
- NNNorm
- NSMul
- Neg
- NegZeroClass
- Nonempty
- Norm
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- SeminormedAddGroup
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero