chore(Topology/Algebra/ContinuousAffineMap): change notation (#12864)

We change the notation for `ContinuousAffineMap` from [→A](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/ContinuousAffineMap.html#ContinuousAffineMap) to `→ᴬ`, so that `→A` can be used for `ContinuousAlgHom` (see #12800).

This seems consistent with the Mathlib notations [→ᵃ](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/AffineSpace/AffineMap.html#AffineMap) for `AffineMap`  and [→ₐ](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Algebra/Hom.html#AlgHom) for `AlgHom`.

Author: mariainesdff

Mathlib/Analysis/Calculus/AffineMap.lean

@@ -27,7 +27,7 @@ variable [NormedAddCommGroup V] [NormedSpace 𝕜 V]
 variable [NormedAddCommGroup W] [NormedSpace 𝕜 W]
 
 /-- A continuous affine map between normed vector spaces is smooth. -/
-theorem contDiff {n : ℕ∞} (f : V →A[𝕜] W) : ContDiff 𝕜 n f := by
+theorem contDiff {n : ℕ∞} (f : V →ᴬ[𝕜] W) : ContDiff 𝕜 n f := by
   rw [f.decomp]
   apply f.contLinear.contDiff.add
   exact contDiff_const

Mathlib/Analysis/Convex/KreinMilman.lean

@@ -108,7 +108,7 @@ theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex
 
 /-- A continuous affine map is surjective from the extreme points of a compact set to the extreme
 points of the image of that set. This inclusion is in general strict. -/
-lemma surjOn_extremePoints_image (f : E →A[ℝ] F) (hs : IsCompact s) :
+lemma surjOn_extremePoints_image (f : E →ᴬ[ℝ] F) (hs : IsCompact s) :
     SurjOn f (extremePoints ℝ s) (extremePoints ℝ (f '' s)) := by
   rintro w hw
   -- The fiber of `w` is nonempty and compact

Mathlib/Analysis/NormedSpace/AddTorsorBases.lean

@@ -46,7 +46,7 @@ theorem continuous_barycentric_coord (i : ι) : Continuous (b.coord i) :=
 #align continuous_barycentric_coord continuous_barycentric_coord
 
 theorem smooth_barycentric_coord (b : AffineBasis ι 𝕜 E) (i : ι) : ContDiff 𝕜 ⊤ (b.coord i) :=
-  (⟨b.coord i, continuous_barycentric_coord b i⟩ : E →A[𝕜] 𝕜).contDiff
+  (⟨b.coord i, continuous_barycentric_coord b i⟩ : E →ᴬ[𝕜] 𝕜).contDiff
 #align smooth_barycentric_coord smooth_barycentric_coord
 
 end Barycentric

Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

@@ -16,9 +16,9 @@ This file develops the theory of continuous affine maps between affine spaces mo
 spaces.
 
 In the particular case that the affine spaces are just normed vector spaces `V`, `W`, we define a
-norm on the space of continuous affine maps by defining the norm of `f : V →A[𝕜] W` to be
+norm on the space of continuous affine maps by defining the norm of `f : V →ᴬ[𝕜] W` to be
 `‖f‖ = max ‖f 0‖ ‖f.cont_linear‖`. This is chosen so that we have a linear isometry:
-`(V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W)`.
+`(V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W)`.
 
 The abstract picture is that for an affine space `P` modelled on a vector space `V`, together with
 a vector space `W`, there is an exact sequence of `𝕜`-modules: `0 → C → A → L → 0` where `C`, `A`
@@ -51,46 +51,46 @@ variable [NormedField R] [NormedSpace R V] [NormedSpace R W] [NormedSpace R W₂
 variable [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [NormedSpace 𝕜 W₂]
 
 /-- The linear map underlying a continuous affine map is continuous. -/
-def contLinear (f : P →A[R] Q) : V →L[R] W :=
+def contLinear (f : P →ᴬ[R] Q) : V →L[R] W :=
   { f.linear with
     toFun := f.linear
     cont := by rw [AffineMap.continuous_linear_iff]; exact f.cont }
 #align continuous_affine_map.cont_linear ContinuousAffineMap.contLinear
 
 @[simp]
-theorem coe_contLinear (f : P →A[R] Q) : (f.contLinear : V → W) = f.linear :=
+theorem coe_contLinear (f : P →ᴬ[R] Q) : (f.contLinear : V → W) = f.linear :=
   rfl
 #align continuous_affine_map.coe_cont_linear ContinuousAffineMap.coe_contLinear
 
 @[simp]
-theorem coe_contLinear_eq_linear (f : P →A[R] Q) :
+theorem coe_contLinear_eq_linear (f : P →ᴬ[R] Q) :
     (f.contLinear : V →ₗ[R] W) = (f : P →ᵃ[R] Q).linear := by ext; rfl
 #align continuous_affine_map.coe_cont_linear_eq_linear ContinuousAffineMap.coe_contLinear_eq_linear
 
 @[simp]
 theorem coe_mk_const_linear_eq_linear (f : P →ᵃ[R] Q) (h) :
-    ((⟨f, h⟩ : P →A[R] Q).contLinear : V → W) = f.linear :=
+    ((⟨f, h⟩ : P →ᴬ[R] Q).contLinear : V → W) = f.linear :=
   rfl
 #align continuous_affine_map.coe_mk_const_linear_eq_linear ContinuousAffineMap.coe_mk_const_linear_eq_linear
 
-theorem coe_linear_eq_coe_contLinear (f : P →A[R] Q) :
+theorem coe_linear_eq_coe_contLinear (f : P →ᴬ[R] Q) :
     ((f : P →ᵃ[R] Q).linear : V → W) = (⇑f.contLinear : V → W) :=
   rfl
 #align continuous_affine_map.coe_linear_eq_coe_cont_linear ContinuousAffineMap.coe_linear_eq_coe_contLinear
 
 @[simp]
-theorem comp_contLinear (f : P →A[R] Q) (g : Q →A[R] Q₂) :
+theorem comp_contLinear (f : P →ᴬ[R] Q) (g : Q →ᴬ[R] Q₂) :
     (g.comp f).contLinear = g.contLinear.comp f.contLinear :=
   rfl
 #align continuous_affine_map.comp_cont_linear ContinuousAffineMap.comp_contLinear
 
 @[simp]
-theorem map_vadd (f : P →A[R] Q) (p : P) (v : V) : f (v +ᵥ p) = f.contLinear v +ᵥ f p :=
+theorem map_vadd (f : P →ᴬ[R] Q) (p : P) (v : V) : f (v +ᵥ p) = f.contLinear v +ᵥ f p :=
   f.map_vadd' p v
 #align continuous_affine_map.map_vadd ContinuousAffineMap.map_vadd
 
 @[simp]
-theorem contLinear_map_vsub (f : P →A[R] Q) (p₁ p₂ : P) : f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂ :=
+theorem contLinear_map_vsub (f : P →ᴬ[R] Q) (p₁ p₂ : P) : f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂ :=
   f.toAffineMap.linearMap_vsub p₁ p₂
 #align continuous_affine_map.cont_linear_map_vsub ContinuousAffineMap.contLinear_map_vsub
 
@@ -99,7 +99,7 @@ theorem const_contLinear (q : Q) : (const R P q).contLinear = 0 :=
   rfl
 #align continuous_affine_map.const_cont_linear ContinuousAffineMap.const_contLinear
 
-theorem contLinear_eq_zero_iff_exists_const (f : P →A[R] Q) :
+theorem contLinear_eq_zero_iff_exists_const (f : P →ᴬ[R] Q) :
     f.contLinear = 0 ↔ ∃ q, f = const R P q := by
   have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 := by
     refine' ⟨fun h => _, fun h => _⟩ <;> ext
@@ -121,43 +121,43 @@ theorem to_affine_map_contLinear (f : V →L[R] W) : f.toContinuousAffineMap.con
 #align continuous_affine_map.to_affine_map_cont_linear ContinuousAffineMap.to_affine_map_contLinear
 
 @[simp]
-theorem zero_contLinear : (0 : P →A[R] W).contLinear = 0 :=
+theorem zero_contLinear : (0 : P →ᴬ[R] W).contLinear = 0 :=
   rfl
 #align continuous_affine_map.zero_cont_linear ContinuousAffineMap.zero_contLinear
 
 @[simp]
-theorem add_contLinear (f g : P →A[R] W) : (f + g).contLinear = f.contLinear + g.contLinear :=
+theorem add_contLinear (f g : P →ᴬ[R] W) : (f + g).contLinear = f.contLinear + g.contLinear :=
   rfl
 #align continuous_affine_map.add_cont_linear ContinuousAffineMap.add_contLinear
 
 @[simp]
-theorem sub_contLinear (f g : P →A[R] W) : (f - g).contLinear = f.contLinear - g.contLinear :=
+theorem sub_contLinear (f g : P →ᴬ[R] W) : (f - g).contLinear = f.contLinear - g.contLinear :=
   rfl
 #align continuous_affine_map.sub_cont_linear ContinuousAffineMap.sub_contLinear
 
 @[simp]
-theorem neg_contLinear (f : P →A[R] W) : (-f).contLinear = -f.contLinear :=
+theorem neg_contLinear (f : P →ᴬ[R] W) : (-f).contLinear = -f.contLinear :=
   rfl
 #align continuous_affine_map.neg_cont_linear ContinuousAffineMap.neg_contLinear
 
 @[simp]
-theorem smul_contLinear (t : R) (f : P →A[R] W) : (t • f).contLinear = t • f.contLinear :=
+theorem smul_contLinear (t : R) (f : P →ᴬ[R] W) : (t • f).contLinear = t • f.contLinear :=
   rfl
 #align continuous_affine_map.smul_cont_linear ContinuousAffineMap.smul_contLinear
 
-theorem decomp (f : V →A[R] W) : (f : V → W) = f.contLinear + Function.const V (f 0) := by
+theorem decomp (f : V →ᴬ[R] W) : (f : V → W) = f.contLinear + Function.const V (f 0) := by
   rcases f with ⟨f, h⟩
   rw [coe_mk_const_linear_eq_linear, coe_mk, f.decomp, Pi.add_apply, LinearMap.map_zero, zero_add,
     ← Function.const_def]
 #align continuous_affine_map.decomp ContinuousAffineMap.decomp
 
 section NormedSpaceStructure
 
-variable (f : V →A[𝕜] W)
+variable (f : V →ᴬ[𝕜] W)
 
 /-- Note that unlike the operator norm for linear maps, this norm is _not_ submultiplicative:
 we do _not_ necessarily have `‖f.comp g‖ ≤ ‖f‖ * ‖g‖`. See `norm_comp_le` for what we can say. -/
-noncomputable instance hasNorm : Norm (V →A[𝕜] W) :=
+noncomputable instance hasNorm : Norm (V →ᴬ[𝕜] W) :=
   ⟨fun f => max ‖f 0‖ ‖f.contLinear‖⟩
 #align continuous_affine_map.has_norm ContinuousAffineMap.hasNorm
 
@@ -182,7 +182,7 @@ theorem norm_eq (h : f 0 = 0) : ‖f‖ = ‖f.contLinear‖ :=
 
 #align continuous_affine_map.norm_eq ContinuousAffineMap.norm_eq
 
-noncomputable instance : NormedAddCommGroup (V →A[𝕜] W) :=
+noncomputable instance : NormedAddCommGroup (V →ᴬ[𝕜] W) :=
   AddGroupNorm.toNormedAddCommGroup
     { toFun := fun f => max ‖f 0‖ ‖f.contLinear‖
       map_zero' := by simp [(ContinuousAffineMap.zero_apply)]
@@ -206,18 +206,18 @@ noncomputable instance : NormedAddCommGroup (V →A[𝕜] W) :=
           rw [h₂]
           rfl }
 
-instance : NormedSpace 𝕜 (V →A[𝕜] W) where
+instance : NormedSpace 𝕜 (V →ᴬ[𝕜] W) where
   norm_smul_le t f := by
     simp only [SMul.smul, norm_def, smul_contLinear, norm_smul]
     -- Porting note: previously all these rewrites were in the `simp only`,
     -- but now they don't fire.
     -- (in fact, `norm_smul` fires, but only once rather than twice!)
-    have : NormedAddCommGroup (V →A[𝕜] W) := inferInstance -- this is necessary for `norm_smul`
+    have : NormedAddCommGroup (V →ᴬ[𝕜] W) := inferInstance -- this is necessary for `norm_smul`
     rw [coe_smul, Pi.smul_apply, norm_smul, norm_smul _ (f.contLinear),
       ← mul_max_of_nonneg _ _ (norm_nonneg t)]
 
 
-theorem norm_comp_le (g : W₂ →A[𝕜] V) : ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by
+theorem norm_comp_le (g : W₂ →ᴬ[𝕜] V) : ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by
   rw [norm_def, max_le_iff]
   constructor
   · calc
@@ -242,7 +242,7 @@ variable (𝕜 V W)
 /-- The space of affine maps between two normed spaces is linearly isometric to the product of the
 codomain with the space of linear maps, by taking the value of the affine map at `(0 : V)` and the
 linear part. -/
-def toConstProdContinuousLinearMap : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W) where
+def toConstProdContinuousLinearMap : (V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W) where
   toFun f := ⟨f 0, f.contLinear⟩
   invFun p := p.2.toContinuousAffineMap + const 𝕜 V p.1
   left_inv f := by
@@ -256,13 +256,13 @@ def toConstProdContinuousLinearMap : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V 
 #align continuous_affine_map.to_const_prod_continuous_linear_map ContinuousAffineMap.toConstProdContinuousLinearMap
 
 @[simp]
-theorem toConstProdContinuousLinearMap_fst (f : V →A[𝕜] W) :
+theorem toConstProdContinuousLinearMap_fst (f : V →ᴬ[𝕜] W) :
     (toConstProdContinuousLinearMap 𝕜 V W f).fst = f 0 :=
   rfl
 #align continuous_affine_map.to_const_prod_continuous_linear_map_fst ContinuousAffineMap.toConstProdContinuousLinearMap_fst
 
 @[simp]
-theorem toConstProdContinuousLinearMap_snd (f : V →A[𝕜] W) :
+theorem toConstProdContinuousLinearMap_snd (f : V →ᴬ[𝕜] W) :
     (toConstProdContinuousLinearMap 𝕜 V W f).snd = f.contLinear :=
   rfl
 #align continuous_affine_map.to_const_prod_continuous_linear_map_snd ContinuousAffineMap.toConstProdContinuousLinearMap_snd