Mathlib Map

Structures · Analysis

SeminormedAddCommGroup

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
Open in Mathlib docs

Extends3

Extended by2

Forgetful instances

Every SeminormedAddCommGroup is also a

Provided automatically by

Concrete types that are instances25

  • ContinuousLinearMap
  • BoundedContinuousFunction
  • WithLp
  • TrivSqZeroExt
  • RestrictScalars
  • PiTensorProduct
  • ZeroAtInftyContinuousMap
  • ContinuousAlternatingMap
  • ContinuousMultilinearMap
  • ContinuousAffineMap
  • PiLp
  • NormedAddGroupHom
  • SemiNormedGrp.carrier
  • RKHS.H₀
  • SemiNormedGrp₁.carrier
  • PositiveLinearMap.PreGNS
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • HasQuotient.Quotient
  • ContinuousMap
  • Shrink
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by3,090

Ancestors65