Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 11:19 a3311136

View on Github →

feat(analysis/normed_space/normed_group_hom): bounded homs between normed groups (#6375) From lean-liquid

Estimated changes

Created src/analysis/normed_space/normed_group_hom.lean

added def add_monoid_hom.mk_normed_group_hom'

added def add_monoid_hom.mk_normed_group_hom

added theorem exists_pos_bound_of_bound

added theorem normed_group_hom.add_apply

added theorem normed_group_hom.antilipschitz_of_bound_by

added theorem normed_group_hom.bound

added def normed_group_hom.bound_by

added theorem normed_group_hom.bound_by_one_of_isometry

added theorem normed_group_hom.bounds_bdd_below

added theorem normed_group_hom.bounds_nonempty

added theorem normed_group_hom.coe_add

added def normed_group_hom.coe_fn_add_hom

added theorem normed_group_hom.coe_inj

added theorem normed_group_hom.coe_inj_iff

added theorem normed_group_hom.coe_injective

added theorem normed_group_hom.coe_mk

added theorem normed_group_hom.coe_mk_normed_group_hom'

added theorem normed_group_hom.coe_mk_normed_group_hom

added theorem normed_group_hom.coe_neg

added theorem normed_group_hom.coe_sub

added theorem normed_group_hom.coe_sum

added theorem normed_group_hom.coe_to_add_monoid_hom

added theorem normed_group_hom.coe_zero

added def normed_group_hom.comp_hom

added theorem normed_group_hom.comp_zero

added theorem normed_group_hom.ext

added theorem normed_group_hom.ext_iff

added def normed_group_hom.id

added def normed_group_hom.incl

added theorem normed_group_hom.isometry_comp

added theorem normed_group_hom.isometry_id

added theorem normed_group_hom.isometry_iff_norm

added theorem normed_group_hom.isometry_of_norm

added theorem normed_group_hom.ker.incl_comp_lift

added def normed_group_hom.ker.lift

added def normed_group_hom.ker

added theorem normed_group_hom.le_of_op_norm_le

added theorem normed_group_hom.le_op_norm

added theorem normed_group_hom.le_op_norm_of_le

added theorem normed_group_hom.lipschitz

added theorem normed_group_hom.lipschitz_of_bound_by

added theorem normed_group_hom.map_add

added theorem normed_group_hom.map_neg

added theorem normed_group_hom.map_sub

added theorem normed_group_hom.map_sum

added theorem normed_group_hom.map_zero

added theorem normed_group_hom.mem_ker

added theorem normed_group_hom.mem_range

added theorem normed_group_hom.mk_normed_group_hom'_bound_by

added theorem normed_group_hom.mk_normed_group_hom_norm_le'

added theorem normed_group_hom.mk_normed_group_hom_norm_le

added theorem normed_group_hom.mk_to_add_monoid_hom

added theorem normed_group_hom.neg_apply

added theorem normed_group_hom.norm_comp_le

added theorem normed_group_hom.norm_def

added theorem normed_group_hom.norm_eq_of_isometry

added theorem normed_group_hom.norm_id

added theorem normed_group_hom.norm_id_le

added theorem normed_group_hom.norm_noninc.bound_by_one

added theorem normed_group_hom.norm_noninc.comp

added theorem normed_group_hom.norm_noninc.id

added def normed_group_hom.norm_noninc

added theorem normed_group_hom.norm_noninc_of_isometry

added def normed_group_hom.op_norm

added theorem normed_group_hom.op_norm_add_le

added theorem normed_group_hom.op_norm_le_bound

added theorem normed_group_hom.op_norm_le_of_lipschitz

added theorem normed_group_hom.op_norm_neg

added theorem normed_group_hom.op_norm_nonneg

added theorem normed_group_hom.op_norm_zero_iff

added def normed_group_hom.range

added theorem normed_group_hom.ratio_le_op_norm

added theorem normed_group_hom.sub_apply

added theorem normed_group_hom.sum_apply

added def normed_group_hom.to_add_monoid_hom

added theorem normed_group_hom.to_add_monoid_hom_injective

added theorem normed_group_hom.to_fun_eq_coe

added theorem normed_group_hom.zero_apply

added theorem normed_group_hom.zero_comp

added structure normed_group_hom

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem exists_pos_bound_of_bound