Commit 2025-04-30 15:39 53c38dde

View on Github →

fix: write ≃ᴬ[k] (instead of ≃ᵃL[k]) for ContinuousAffineEquiv (#24357) This PR changes the notation for ContinuousAffineEquiv from ≃ᵃL[k] to ≃ᴬ[k]. This is consistent with the notation for ContinuousAffineMap, namely →ᴬ[k]. I would like to change the notation for continuous bundled functions in the future (see #mathlib4 > RFC: notation for continuous maps in algebra), but before that we should at least have the Map and Equiv versions be consistent.

Estimated changes

Modified Mathlib/Analysis/Convex/AmpleSet.lean

modified theorem AmpleSet.image

modified theorem AmpleSet.image_iff

modified theorem AmpleSet.preimage

modified theorem AmpleSet.preimage_iff

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

modified def ContinuousAffineEquiv.Simps.apply

modified def ContinuousAffineEquiv.Simps.symm_apply

modified theorem ContinuousAffineEquiv.apply_eq_iff_eq

modified theorem ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply

modified theorem ContinuousAffineEquiv.apply_symm_apply

modified theorem ContinuousAffineEquiv.coe_coe

modified theorem ContinuousAffineEquiv.coe_injective

modified theorem ContinuousAffineEquiv.coe_toContinuousAffineMap

modified theorem ContinuousAffineEquiv.coe_toEquiv

modified theorem ContinuousAffineEquiv.coe_trans

modified def ContinuousAffineEquiv.constVAdd

modified theorem ContinuousAffineEquiv.eq_symm_apply

modified theorem ContinuousAffineEquiv.ext

modified theorem ContinuousAffineEquiv.image_preimage

modified theorem ContinuousAffineEquiv.image_symm

modified theorem ContinuousAffineEquiv.image_symm_image

modified theorem ContinuousAffineEquiv.preimage_image

modified theorem ContinuousAffineEquiv.preimage_symm

modified def ContinuousAffineEquiv.refl

modified theorem ContinuousAffineEquiv.refl_trans

modified theorem ContinuousAffineEquiv.self_trans_symm

modified def ContinuousAffineEquiv.symm

modified theorem ContinuousAffineEquiv.symm_apply_apply

modified theorem ContinuousAffineEquiv.symm_apply_eq

modified theorem ContinuousAffineEquiv.symm_bijective

modified theorem ContinuousAffineEquiv.symm_image_image

modified theorem ContinuousAffineEquiv.symm_symm

modified theorem ContinuousAffineEquiv.symm_symm_apply

modified theorem ContinuousAffineEquiv.symm_toAffineEquiv

modified theorem ContinuousAffineEquiv.symm_toEquiv

modified theorem ContinuousAffineEquiv.symm_trans_self

modified theorem ContinuousAffineEquiv.toAffineEquiv_injective

modified def ContinuousAffineEquiv.toContinuousAffineMap

modified theorem ContinuousAffineEquiv.toContinuousAffineMap_toAffineMap

modified theorem ContinuousAffineEquiv.toContinuousAffineMap_toContinuousMap

modified def ContinuousAffineEquiv.toHomeomorph

modified def ContinuousAffineEquiv.trans

modified theorem ContinuousAffineEquiv.trans_apply

modified theorem ContinuousAffineEquiv.trans_assoc

modified theorem ContinuousAffineEquiv.trans_refl

modified theorem ContinuousAffineEquiv.trans_toContinuousAffineMap

modified def ContinuousLinearEquiv.toContinuousAffineEquiv