Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-18 04:50 1a2781a7

View on Github →

feat(analysis/normed_space): the category of seminormed groups (#7617) From LTE, along with adding SemiNormedGroup₁, the subcategory of norm non-increasing maps.

Estimated changes

Created src/analysis/normed_space/SemiNormedGroup.lean

added theorem SemiNormedGroup.coe_id

added theorem SemiNormedGroup.coe_of

added def SemiNormedGroup.of

added def SemiNormedGroup

added theorem SemiNormedGroup₁.coe_comp

added theorem SemiNormedGroup₁.coe_id

added theorem SemiNormedGroup₁.coe_of

added theorem SemiNormedGroup₁.hom_ext

added theorem SemiNormedGroup₁.iso_isometry

added def SemiNormedGroup₁.mk_hom

added theorem SemiNormedGroup₁.mk_hom_apply

added def SemiNormedGroup₁.mk_iso

added def SemiNormedGroup₁.of

added theorem SemiNormedGroup₁.zero_apply

added def SemiNormedGroup₁

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.norm_noninc.zero