# mathlib3documentation

analysis.normed.group.SemiNormedGroup

# The category of seminormed groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for SemiNormedGroup
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

Construct a bundled SemiNormedGroup from the underlying type and typeclass.

Equations
Instances for ↥SemiNormedGroup.of
@[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]
def SemiNormedGroup.of_unique (V : Type u) [i : unique V] :
Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup.zero_apply {V W : SemiNormedGroup} (x : V) :
0 x = 0
@[protected, instance]
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
Instances for SemiNormedGroup₁
@[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
Instances for ↥SemiNormedGroup₁.of
@[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]
theorem SemiNormedGroup₁.mk_iso_inv {M N : SemiNormedGroup} (f : M N)  :
i').inv =
@[simp]
theorem SemiNormedGroup₁.mk_iso_hom {M N : SemiNormedGroup} (f : M N)  :
i').hom =
noncomputable def SemiNormedGroup₁.mk_iso {M N : SemiNormedGroup} (f : M N)  :

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]
def SemiNormedGroup₁.of_unique (V : Type u) [i : unique V] :
Equations
@[protected, instance]
Equations
@[simp]
theorem SemiNormedGroup₁.zero_apply {V W : SemiNormedGroup₁} (x : V) :
0 x = 0
@[protected, instance]