Commit 2023-06-08 07:20 b8c76856

View on Github →

feat: port Topology.Algebra.ContinuousAffineMap (#3277)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ContinuousAffineMap.lean

added theorem ContinuousAffineMap.add_apply

added theorem ContinuousAffineMap.coe_add

added theorem ContinuousAffineMap.coe_affineMap_mk

added theorem ContinuousAffineMap.coe_comp

added theorem ContinuousAffineMap.coe_const

added theorem ContinuousAffineMap.coe_continuousMap_mk

added theorem ContinuousAffineMap.coe_injective

added theorem ContinuousAffineMap.coe_mk

added theorem ContinuousAffineMap.coe_neg

added theorem ContinuousAffineMap.coe_smul

added theorem ContinuousAffineMap.coe_sub

added theorem ContinuousAffineMap.coe_to_affineMap

added theorem ContinuousAffineMap.coe_to_continuousMap

added theorem ContinuousAffineMap.coe_zero

added def ContinuousAffineMap.comp

added theorem ContinuousAffineMap.comp_apply

added theorem ContinuousAffineMap.congr_fun

added def ContinuousAffineMap.const

added theorem ContinuousAffineMap.ext

added theorem ContinuousAffineMap.ext_iff

added theorem ContinuousAffineMap.mk_coe

added theorem ContinuousAffineMap.neg_apply

added theorem ContinuousAffineMap.smul_apply

added theorem ContinuousAffineMap.sub_apply

added def ContinuousAffineMap.toContinuousMap

added theorem ContinuousAffineMap.toContinuousMap_coe

added theorem ContinuousAffineMap.toFun_eq_coe

added theorem ContinuousAffineMap.to_affineMap_injective

added theorem ContinuousAffineMap.to_continuousMap_injective

added theorem ContinuousAffineMap.zero_apply

added structure ContinuousAffineMap

added theorem ContinuousLinearMap.coe_toContinuousAffineMap

added def ContinuousLinearMap.toContinuousAffineMap

added theorem ContinuousLinearMap.toContinuousAffineMap_map_zero