mathlib documentation

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.

@[protected, instance]
Equations

Construct a bundled SemiNormedGroup from the underlying type and typeclass.

Equations
Instances for SemiNormedGroup.of
@[simp]
@[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
@[simp]
theorem SemiNormedGroup.zero_apply {V W : SemiNormedGroup} (x : V) :
0 x = 0
@[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
@[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
@[simp]
theorem SemiNormedGroup₁.zero_apply {V W : SemiNormedGroup₁} (x : V) :
0 x = 0