Commit 2021-11-12 16:30 62621659

View on Github →

feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/analysis/normed_space/continuous_affine_map.lean

added theorem continuous_affine_map.add_cont_linear

added theorem continuous_affine_map.coe_cont_linear

modified theorem continuous_affine_map.coe_linear_eq_coe_cont_linear

added theorem continuous_affine_map.comp_cont_linear

added theorem continuous_affine_map.decomp

added theorem continuous_affine_map.neg_cont_linear

added theorem continuous_affine_map.norm_comp_le

added theorem continuous_affine_map.norm_cont_linear_le

added theorem continuous_affine_map.norm_def

added theorem continuous_affine_map.norm_eq

added theorem continuous_affine_map.norm_image_zero_le

added theorem continuous_affine_map.smul_cont_linear

added theorem continuous_affine_map.sub_cont_linear

added theorem continuous_affine_map.to_affine_map_cont_linear

added theorem continuous_affine_map.to_const_prod_continuous_linear_map_fst

added theorem continuous_affine_map.to_const_prod_continuous_linear_map_snd

added theorem continuous_affine_map.zero_cont_linear

Modified src/topology/algebra/continuous_affine_map.lean

added theorem continuous_affine_map.add_apply

added theorem continuous_affine_map.coe_add

added theorem continuous_affine_map.coe_neg

added theorem continuous_affine_map.coe_smul

added theorem continuous_affine_map.coe_sub

added theorem continuous_affine_map.coe_zero

added theorem continuous_affine_map.neg_apply

added theorem continuous_affine_map.smul_apply

added theorem continuous_affine_map.sub_apply

added theorem continuous_affine_map.zero_apply

added theorem continuous_linear_map.coe_to_continuous_affine_map

added def continuous_linear_map.to_continuous_affine_map

added theorem continuous_linear_map.to_continuous_affine_map_map_zero