mathlib documentation

analysis.normed_space.SemiNormedGroup

The category of seminormed groups #

We define SemiNormedGroup, the category of seminormed groups and normed group homs between them, as well as SemiNormedGroup₁, the subcategory of norm non-increasing morphisms.

def SemiNormedGroup  :
Type (u+1)

The category of seminormed abelian groups and bounded group homomorphisms.

Equations

Construct a bundled SemiNormedGroup from the underlying type and typeclass.

Equations
@[simp]
@[simp]
@[simp]
theorem SemiNormedGroup.coe_comp {M N K : SemiNormedGroup} (f : M N) (g : N K) :
(f g) = g f
@[instance]
Equations
@[simp]
theorem SemiNormedGroup.zero_apply {V W : SemiNormedGroup} (x : V) :
0 x = 0
def SemiNormedGroup₁  :
Type (u+1)

SemiNormedGroup₁ is a type synonym for SemiNormedGroup, which we shall equip with the category structure consisting only of the norm non-increasing maps.

Equations
@[instance]
Equations
@[ext]
theorem SemiNormedGroup₁.hom_ext {M N : SemiNormedGroup₁} (f g : M N) (w : f = g) :
f = g
@[instance]
Equations

Construct a bundled SemiNormedGroup₁ from the underlying type and typeclass.

Equations
@[instance]
Equations
@[simp]
theorem SemiNormedGroup₁.coe_comp {M N K : SemiNormedGroup₁} (f : M N) (g : N K) :
(f g) = g f
@[instance]
Equations
@[simp]
theorem SemiNormedGroup₁.zero_apply {V W : SemiNormedGroup₁} (x : V) :
0 x = 0