Commit 2024-04-05 21:50 1b545f0b

View on Github →

feat: continuous affine equivalences (#11341)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Created Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

added def ContinuousAffineEquiv.Simps.apply

added def ContinuousAffineEquiv.Simps.coe

added theorem ContinuousAffineEquiv.apply_eq_iff_eq

added theorem ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply

added theorem ContinuousAffineEquiv.apply_symm_apply

added theorem ContinuousAffineEquiv.coe_coe

added theorem ContinuousAffineEquiv.coe_injective

added theorem ContinuousAffineEquiv.coe_refl

added theorem ContinuousAffineEquiv.coe_toEquiv

added theorem ContinuousAffineEquiv.coe_trans

added def ContinuousAffineEquiv.constVAdd

added theorem ContinuousAffineEquiv.constVAdd_coe

added theorem ContinuousAffineEquiv.eq_symm_apply

added theorem ContinuousAffineEquiv.ext

added theorem ContinuousAffineEquiv.ext_iff

added theorem ContinuousAffineEquiv.image_symm

added theorem ContinuousAffineEquiv.preimage_symm

added def ContinuousAffineEquiv.refl

added theorem ContinuousAffineEquiv.refl_apply

added theorem ContinuousAffineEquiv.refl_symm

added theorem ContinuousAffineEquiv.refl_trans

added theorem ContinuousAffineEquiv.self_trans_symm

added def ContinuousAffineEquiv.symm

added theorem ContinuousAffineEquiv.symm_apply_apply

added theorem ContinuousAffineEquiv.symm_apply_eq

added theorem ContinuousAffineEquiv.symm_refl

added theorem ContinuousAffineEquiv.symm_symm

added theorem ContinuousAffineEquiv.symm_symm_apply

added theorem ContinuousAffineEquiv.symm_toAffineEquiv

added theorem ContinuousAffineEquiv.symm_toEquiv

added theorem ContinuousAffineEquiv.symm_trans_self

added theorem ContinuousAffineEquiv.toAffineEquiv_injective

added theorem ContinuousAffineEquiv.toAffineEquiv_refl

added theorem ContinuousAffineEquiv.toEquiv_refl

added def ContinuousAffineEquiv.toHomeomorph

added def ContinuousAffineEquiv.trans

added theorem ContinuousAffineEquiv.trans_apply

added theorem ContinuousAffineEquiv.trans_assoc

added theorem ContinuousAffineEquiv.trans_refl

added structure ContinuousAffineEquiv

added theorem ContinuousLinearEquiv.coe_toContinuousAffineEquiv

added def ContinuousLinearEquiv.toContinuousAffineEquiv