Commit 2023-06-09 09:11 697b3954

View on Github →

feat: port Analysis.NormedSpace.ContinuousAffineMap (#4867)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

added theorem ContinuousAffineMap.add_contLinear

added theorem ContinuousAffineMap.coe_contLinear

added theorem ContinuousAffineMap.coe_contLinear_eq_linear

added theorem ContinuousAffineMap.coe_linear_eq_coe_contLinear

added theorem ContinuousAffineMap.coe_mk_const_linear_eq_linear

added theorem ContinuousAffineMap.comp_contLinear

added theorem ContinuousAffineMap.const_contLinear

added def ContinuousAffineMap.contLinear

added theorem ContinuousAffineMap.contLinear_eq_zero_iff_exists_const

added theorem ContinuousAffineMap.contLinear_map_vsub

added theorem ContinuousAffineMap.decomp

added theorem ContinuousAffineMap.map_vadd

added theorem ContinuousAffineMap.neg_contLinear

added theorem ContinuousAffineMap.norm_comp_le

added theorem ContinuousAffineMap.norm_contLinear_le

added theorem ContinuousAffineMap.norm_def

added theorem ContinuousAffineMap.norm_eq

added theorem ContinuousAffineMap.norm_image_zero_le

added theorem ContinuousAffineMap.smul_contLinear

added theorem ContinuousAffineMap.sub_contLinear

added def ContinuousAffineMap.toConstProdContinuousLinearMap

added theorem ContinuousAffineMap.toConstProdContinuousLinearMap_fst

added theorem ContinuousAffineMap.toConstProdContinuousLinearMap_snd

added theorem ContinuousAffineMap.to_affine_map_contLinear

added theorem ContinuousAffineMap.zero_contLinear