Structures · Analysis
SeminormedAddGroup
A seminormed group is an additive group endowed with a norm for which dist x y = ‖-x + y‖
defines a pseudometric space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds dist_eq
Extends3
Extended by2
Forgetful instances
Every SeminormedAddGroup is also a
Provided automatically by
Concrete types that are instances6
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by324
- norm_nonneg
- norm_zero
- norm_neg
- dist_zero_right
- norm_add_le
- dist_eq_norm_neg_add
- Continuous.norm
- Filter.Tendsto.norm
- norm_sub_rev
- nnnorm_zero
- ofReal_norm
- abs_norm
- continuous_norm
- coe_nnnorm
- tendsto_zero_iff_norm_tendsto_zero
- ContinuousOn.norm
- norm_sub_le
- edist_zero_right
- norm_smul_le
- mem_ball_zero_iff
- toReal_enorm
- norm_map
- Asymptotics.isLittleO_one_iff
- pi_norm_le_iff_of_nonneg
- AddMonoidHomClass.isometry_of_norm
- isBounded_iff_forall_norm_le
- norm_le_pi_norm
- dist_zero
- mem_closedBall_zero_iff
- dist_zero_left
- nnnorm_smul
- Isometry.norm_map_of_map_zero
- nnnorm_neg
- mem_sphere_zero_iff_norm
- tendsto_norm_atTop_iff_cobounded
- norm_add_le_of_le
- Pi.nnnorm_def
- norm_eq_of_mem_sphere
- dist_self_add_left
- norm_indicator_eq_indicator_norm
- tendsto_norm_cobounded_atTop
- nnnorm_smul_le
- ContinuousAt.norm
- enorm_neg
- norm_add₃_le
- continuous_nnnorm
- approxAddOrderOf
- norm_of_subsingleton
- mem_eball_zero_iff
- IsCompact.exists_bound_of_continuousOn
Ancestors54
- Add
- AddAction
- AddCancelMonoid
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- EDist
- ENorm
- HAdd
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- LocallyPathConnectedSpace
- NNDist
- NNNorm
- NSMul
- Neg
- NegZeroClass
- Nonempty
- Norm
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero