Commit 2023-03-09 00:44 f099b892

View on Github →

feat: port Analysis.Normed.Group.Seminorm (#2400)

depends on: #2401
depends on: #2419

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/Seminorm.lean

added theorem AddGroupNorm.apply_one

added structure AddGroupNorm

added theorem AddGroupSeminorm.apply_one

added theorem AddGroupSeminorm.coe_smul

added theorem AddGroupSeminorm.smul_apply

added theorem AddGroupSeminorm.smul_sup

added structure AddGroupSeminorm

added theorem GroupNorm.add_apply

added theorem GroupNorm.apply_one

added theorem GroupNorm.coe_add

added theorem GroupNorm.coe_le_coe

added theorem GroupNorm.coe_lt_coe

added theorem GroupNorm.coe_sup

added theorem GroupNorm.ext

added theorem GroupNorm.le_def

added theorem GroupNorm.lt_def

added theorem GroupNorm.sup_apply

added theorem GroupNorm.toGroupSeminorm_eq_coe

added structure GroupNorm

added theorem GroupSeminorm.add_apply

added theorem GroupSeminorm.add_comp

added theorem GroupSeminorm.apply_one

added theorem GroupSeminorm.coe_add

added theorem GroupSeminorm.coe_comp

added theorem GroupSeminorm.coe_le_coe

added theorem GroupSeminorm.coe_lt_coe

added theorem GroupSeminorm.coe_smul

added theorem GroupSeminorm.coe_sup

added theorem GroupSeminorm.coe_zero

added def GroupSeminorm.comp

added theorem GroupSeminorm.comp_apply

added theorem GroupSeminorm.comp_assoc

added theorem GroupSeminorm.comp_id

added theorem GroupSeminorm.comp_mono

added theorem GroupSeminorm.comp_mul_le

added theorem GroupSeminorm.comp_zero

added theorem GroupSeminorm.ext

added theorem GroupSeminorm.inf_apply

added theorem GroupSeminorm.le_def

added theorem GroupSeminorm.lt_def

added theorem GroupSeminorm.mul_bddBelow_range_add

added theorem GroupSeminorm.smul_apply

added theorem GroupSeminorm.smul_sup

added theorem GroupSeminorm.sup_apply

added theorem GroupSeminorm.toFun_eq_coe

added theorem GroupSeminorm.zero_apply

added theorem GroupSeminorm.zero_comp

added structure GroupSeminorm

added theorem NonarchAddGroupNorm.apply_one

added theorem NonarchAddGroupNorm.coe_le_coe

added theorem NonarchAddGroupNorm.coe_lt_coe

added theorem NonarchAddGroupNorm.coe_sup

added theorem NonarchAddGroupNorm.ext

added theorem NonarchAddGroupNorm.le_def

added theorem NonarchAddGroupNorm.lt_def

added theorem NonarchAddGroupNorm.sup_apply

added theorem NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe

added structure NonarchAddGroupNorm

added theorem NonarchAddGroupSeminorm.add_bddBelow_range_add

added theorem NonarchAddGroupSeminorm.apply_one

added theorem NonarchAddGroupSeminorm.coe_le_coe

added theorem NonarchAddGroupSeminorm.coe_lt_coe

added theorem NonarchAddGroupSeminorm.coe_smul

added theorem NonarchAddGroupSeminorm.coe_sup

added theorem NonarchAddGroupSeminorm.coe_zero

added theorem NonarchAddGroupSeminorm.ext

added theorem NonarchAddGroupSeminorm.le_def

added theorem NonarchAddGroupSeminorm.lt_def

added theorem NonarchAddGroupSeminorm.smul_apply

added theorem NonarchAddGroupSeminorm.smul_sup

added theorem NonarchAddGroupSeminorm.sup_apply

added theorem NonarchAddGroupSeminorm.toZeroHom_eq_coe

added theorem NonarchAddGroupSeminorm.zero_apply

added structure NonarchAddGroupSeminorm

added theorem map_sub_le_max