Commit 2022-06-23 14:10 cff439d8

View on Github →

feat(analysis/seminorm): add add_group_seminorm (#14336) We introduce add_group_seminorm and refactor seminorm to extend this new definition. This new add_group_seminorm structure will also be used in #14115 to define ring_seminorm.

Estimated changes

Modified counterexamples/seminorm_lattice_not_distrib.lean

Modified src/analysis/convex/gauge.lean

Modified src/analysis/seminorm.lean

added theorem add_group_seminorm.add_apply

added theorem add_group_seminorm.add_comp

added theorem add_group_seminorm.coe_add

added theorem add_group_seminorm.coe_comp

added theorem add_group_seminorm.coe_smul

added theorem add_group_seminorm.coe_sup

added theorem add_group_seminorm.coe_zero

added def add_group_seminorm.comp

added theorem add_group_seminorm.comp_add_le

added theorem add_group_seminorm.comp_apply

added theorem add_group_seminorm.comp_comp

added theorem add_group_seminorm.comp_id

added theorem add_group_seminorm.comp_mono

added theorem add_group_seminorm.comp_zero

added theorem add_group_seminorm.ext

added theorem add_group_seminorm.inf_apply

added theorem add_group_seminorm.le_def

added theorem add_group_seminorm.le_insert'

added theorem add_group_seminorm.le_insert

added theorem add_group_seminorm.lt_def

added theorem add_group_seminorm.smul_apply

added theorem add_group_seminorm.smul_sup

added theorem add_group_seminorm.sub_rev

added theorem add_group_seminorm.sup_apply

added theorem add_group_seminorm.zero_apply

added theorem add_group_seminorm.zero_comp

added structure add_group_seminorm

added theorem coe_norm_add_group_seminorm

added def norm_add_group_seminorm

modified def norm_seminorm

modified theorem seminorm.ball_bot

modified theorem seminorm.ball_finset_sup

added theorem seminorm.comp_add_le

deleted theorem seminorm.comp_triangle

deleted theorem seminorm.nonneg

added def seminorm.of

modified structure seminorm