Commit 2024-05-16 21:59 0ce4969e

View on Github →

chore(Topology/Algebra/ContinuousAffineMap): change notation (#12864) We change the notation for ContinuousAffineMap from →A to →ᴬ, so that →A can be used for ContinuousAlgHom (see #12800). This seems consistent with the Mathlib notations →ᵃ for AffineMap and →ₐ for AlgHom.

Estimated changes

Modified Mathlib/Analysis/Calculus/AffineMap.lean

modified theorem ContinuousAffineMap.contDiff

Modified Mathlib/Analysis/Convex/KreinMilman.lean

modified theorem surjOn_extremePoints_image

Modified Mathlib/Analysis/NormedSpace/AddTorsorBases.lean

Modified Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

modified theorem ContinuousAffineMap.add_contLinear

modified theorem ContinuousAffineMap.coe_contLinear

modified theorem ContinuousAffineMap.coe_contLinear_eq_linear

modified theorem ContinuousAffineMap.coe_linear_eq_coe_contLinear

modified theorem ContinuousAffineMap.comp_contLinear

modified def ContinuousAffineMap.contLinear

modified theorem ContinuousAffineMap.contLinear_eq_zero_iff_exists_const

modified theorem ContinuousAffineMap.contLinear_map_vsub

modified theorem ContinuousAffineMap.decomp

modified theorem ContinuousAffineMap.map_vadd

modified theorem ContinuousAffineMap.neg_contLinear

modified theorem ContinuousAffineMap.norm_comp_le

modified theorem ContinuousAffineMap.smul_contLinear

modified theorem ContinuousAffineMap.sub_contLinear

modified def ContinuousAffineMap.toConstProdContinuousLinearMap

modified theorem ContinuousAffineMap.toConstProdContinuousLinearMap_fst

modified theorem ContinuousAffineMap.toConstProdContinuousLinearMap_snd

modified theorem ContinuousAffineMap.zero_contLinear

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

modified theorem ContinuousAffineMap.add_apply

modified theorem ContinuousAffineMap.coe_add

modified theorem ContinuousAffineMap.coe_affineMap_mk

modified theorem ContinuousAffineMap.coe_comp

modified theorem ContinuousAffineMap.coe_continuousMap_mk

modified theorem ContinuousAffineMap.coe_injective

modified theorem ContinuousAffineMap.coe_mk

modified theorem ContinuousAffineMap.coe_neg

modified theorem ContinuousAffineMap.coe_smul

modified theorem ContinuousAffineMap.coe_sub

modified theorem ContinuousAffineMap.coe_to_affineMap

modified theorem ContinuousAffineMap.coe_to_continuousMap

modified theorem ContinuousAffineMap.coe_zero

modified def ContinuousAffineMap.comp

modified theorem ContinuousAffineMap.comp_apply

modified theorem ContinuousAffineMap.congr_fun

modified def ContinuousAffineMap.const

modified theorem ContinuousAffineMap.ext

modified theorem ContinuousAffineMap.ext_iff

modified theorem ContinuousAffineMap.mk_coe

modified theorem ContinuousAffineMap.neg_apply

modified theorem ContinuousAffineMap.smul_apply

modified theorem ContinuousAffineMap.sub_apply

modified def ContinuousAffineMap.toContinuousMap

modified theorem ContinuousAffineMap.toContinuousMap_coe

modified theorem ContinuousAffineMap.toFun_eq_coe

modified theorem ContinuousAffineMap.to_affineMap_injective

modified theorem ContinuousAffineMap.to_continuousMap_injective

modified theorem ContinuousAffineMap.zero_apply

modified def ContinuousLinearMap.toContinuousAffineMap