Commit 2023-03-10 07:49 187a9071

View on Github →

feat: port Analysis.Normed.Group.Hom (#2748)

Estimated changes

Modified Mathlib.lean

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

added def AddMonoidHom.mkNormedAddGroupHom'

added def AddMonoidHom.mkNormedAddGroupHom

added theorem NormedAddGroupHom.Equalizer.comm_sq₂

added theorem NormedAddGroupHom.Equalizer.comp_ι_eq

added def NormedAddGroupHom.Equalizer.lift

added def NormedAddGroupHom.Equalizer.liftEquiv

added theorem NormedAddGroupHom.Equalizer.lift_normNoninc

added def NormedAddGroupHom.Equalizer.map

added theorem NormedAddGroupHom.Equalizer.map_comp_map

added theorem NormedAddGroupHom.Equalizer.map_id

added theorem NormedAddGroupHom.Equalizer.map_normNoninc

added theorem NormedAddGroupHom.Equalizer.norm_lift_le

added theorem NormedAddGroupHom.Equalizer.norm_map_le

added def NormedAddGroupHom.Equalizer.ι

added theorem NormedAddGroupHom.Equalizer.ι_comp_lift

added theorem NormedAddGroupHom.Equalizer.ι_comp_map

added theorem NormedAddGroupHom.Equalizer.ι_normNoninc

added theorem NormedAddGroupHom.NormNoninc.comp

added theorem NormedAddGroupHom.NormNoninc.id

added theorem NormedAddGroupHom.NormNoninc.neg_iff

added theorem NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one

added theorem NormedAddGroupHom.NormNoninc.zero

added def NormedAddGroupHom.NormNoninc

added theorem NormedAddGroupHom.SurjectiveOnWith.exists_pos

added theorem NormedAddGroupHom.SurjectiveOnWith.mono

added theorem NormedAddGroupHom.SurjectiveOnWith.surjOn

added def NormedAddGroupHom.SurjectiveOnWith

added theorem NormedAddGroupHom.add_apply

added theorem NormedAddGroupHom.antilipschitz_of_norm_ge

added theorem NormedAddGroupHom.bound

added theorem NormedAddGroupHom.bounds_bddBelow

added theorem NormedAddGroupHom.bounds_nonempty

added def NormedAddGroupHom.coeAddHom

added theorem NormedAddGroupHom.coe_add

added theorem NormedAddGroupHom.coe_comp

added theorem NormedAddGroupHom.coe_id

added theorem NormedAddGroupHom.coe_inj

added theorem NormedAddGroupHom.coe_inj_iff

added theorem NormedAddGroupHom.coe_injective

added theorem NormedAddGroupHom.coe_ker

added theorem NormedAddGroupHom.coe_mk

added theorem NormedAddGroupHom.coe_mkNormedAddGroupHom'

added theorem NormedAddGroupHom.coe_mkNormedAddGroupHom

added theorem NormedAddGroupHom.coe_neg

added theorem NormedAddGroupHom.coe_nsmul

added theorem NormedAddGroupHom.coe_smul

added theorem NormedAddGroupHom.coe_sub

added theorem NormedAddGroupHom.coe_sum

added theorem NormedAddGroupHom.coe_toAddMonoidHom

added theorem NormedAddGroupHom.coe_zero

added theorem NormedAddGroupHom.coe_zsmul

added def NormedAddGroupHom.compHom

added theorem NormedAddGroupHom.comp_assoc

added theorem NormedAddGroupHom.comp_range

added theorem NormedAddGroupHom.comp_zero

added def NormedAddGroupHom.equalizer

added theorem NormedAddGroupHom.ext

added theorem NormedAddGroupHom.ext_iff

added def NormedAddGroupHom.id

added def NormedAddGroupHom.incl

added theorem NormedAddGroupHom.incl_range

added theorem NormedAddGroupHom.isClosed_ker

added theorem NormedAddGroupHom.isometry_comp

added theorem NormedAddGroupHom.isometry_id

added theorem NormedAddGroupHom.ker.incl_comp_lift

added def NormedAddGroupHom.ker.lift

added def NormedAddGroupHom.ker

added theorem NormedAddGroupHom.ker_zero

added theorem NormedAddGroupHom.le_of_op_norm_le

added theorem NormedAddGroupHom.le_opNorm

added theorem NormedAddGroupHom.le_opNorm_of_le

added theorem NormedAddGroupHom.lipschitz

added theorem NormedAddGroupHom.mem_ker

added theorem NormedAddGroupHom.mem_range

added theorem NormedAddGroupHom.mem_range_self

added theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le'

added theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le

added theorem NormedAddGroupHom.mk_toAddMonoidHom

added theorem NormedAddGroupHom.neg_apply

added theorem NormedAddGroupHom.normNoninc_of_isometry

added theorem NormedAddGroupHom.norm_comp_le

added theorem NormedAddGroupHom.norm_comp_le_of_le'

added theorem NormedAddGroupHom.norm_comp_le_of_le

added theorem NormedAddGroupHom.norm_def

added theorem NormedAddGroupHom.norm_eq_of_isometry

added theorem NormedAddGroupHom.norm_id

added theorem NormedAddGroupHom.norm_id_le

added theorem NormedAddGroupHom.norm_id_of_nontrivial_seminorm

added theorem NormedAddGroupHom.norm_incl

added theorem NormedAddGroupHom.nsmul_apply

added def NormedAddGroupHom.opNorm

added theorem NormedAddGroupHom.opNorm_add_le

added theorem NormedAddGroupHom.opNorm_eq_of_bounds

added theorem NormedAddGroupHom.opNorm_le_bound

added theorem NormedAddGroupHom.opNorm_le_of_lipschitz

added theorem NormedAddGroupHom.opNorm_neg

added theorem NormedAddGroupHom.opNorm_nonneg

added theorem NormedAddGroupHom.opNorm_zero

added theorem NormedAddGroupHom.opNorm_zero_iff

added def NormedAddGroupHom.range

added theorem NormedAddGroupHom.range_comp_incl_top

added theorem NormedAddGroupHom.ratio_le_opNorm

added theorem NormedAddGroupHom.smul_apply

added theorem NormedAddGroupHom.sub_apply

added theorem NormedAddGroupHom.sum_apply

added def NormedAddGroupHom.toAddMonoidHom

added theorem NormedAddGroupHom.toAddMonoidHom_injective

added theorem NormedAddGroupHom.toFun_eq_coe

added theorem NormedAddGroupHom.zero_apply

added theorem NormedAddGroupHom.zero_comp

added theorem NormedAddGroupHom.zsmul_apply

added structure NormedAddGroupHom

added theorem exists_pos_bound_of_bound