# mathlibdocumentation

analysis.normed.group.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
@[protected, instance]
noncomputable def SemiNormedGroup.bundled_hom  :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
def SemiNormedGroup.of (M : Type u)  :

Construct a bundled SemiNormedGroup from the underlying type and typeclass.

Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup.coe_of (V : Type u)  :
= V
@[simp]
@[simp]
theorem SemiNormedGroup.coe_comp {M N K : SemiNormedGroup} (f : M N) (g : N K) :
(f g) = g f
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup.zero_apply {V W : SemiNormedGroup} (x : V) :
0 x = 0
@[protected, instance]
Equations
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
@[protected, instance]
Equations
@[protected, instance]
Equations
@[ext]
theorem SemiNormedGroup₁.hom_ext {M N : SemiNormedGroup₁} (f g : M N) (w : f = g) :
f = g
@[protected, instance]
Equations

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

Equations
@[protected, instance]
Equations
def SemiNormedGroup₁.mk_hom {M N : SemiNormedGroup} (f : M N)  :

Promote a morphism in SemiNormedGroup to a morphism in SemiNormedGroup₁.

Equations
@[simp]
theorem SemiNormedGroup₁.mk_hom_apply {M N : SemiNormedGroup} (f : M N) (x : ) :
x = f x
@[simp]
@[simp]
noncomputable def SemiNormedGroup₁.mk_iso {M N : SemiNormedGroup} (f : M N) (i' : normed_group_hom.norm_noninc f.inv) :

Promote an isomorphism in SemiNormedGroup to an isomorphism in SemiNormedGroup₁.

Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup₁.coe_of (V : Type u)  :
@[simp]
theorem SemiNormedGroup₁.coe_comp {M N K : SemiNormedGroup₁} (f : M N) (g : N K) :
(f g) = g f
@[simp]
theorem SemiNormedGroup₁.coe_comp' {M N K : SemiNormedGroup₁} (f : M N) (g : N K) :
(f g) = g.comp f
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup₁.zero_apply {V W : SemiNormedGroup₁} (x : V) :
0 x = 0
@[protected, instance]
Equations