Commit 2023-05-19 18:00 d1691c36

View on Github →

feat: port Analysis.NormedSpace.AffineIsometry (#3651)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/AffineIsometry.lean

added theorem AffineIsometry.coeFn_injective

added theorem AffineIsometry.coe_comp

added theorem AffineIsometry.coe_id

added theorem AffineIsometry.coe_mul

added theorem AffineIsometry.coe_one

added theorem AffineIsometry.coe_toAffineMap

added def AffineIsometry.comp

added theorem AffineIsometry.comp_assoc

added theorem AffineIsometry.comp_continuous_iff

added theorem AffineIsometry.comp_id

added theorem AffineIsometry.diam_image

added theorem AffineIsometry.diam_range

added theorem AffineIsometry.dist_map

added theorem AffineIsometry.ediam_image

added theorem AffineIsometry.ediam_range

added theorem AffineIsometry.edist_map

added theorem AffineIsometry.ext

added def AffineIsometry.id

added theorem AffineIsometry.id_apply

added theorem AffineIsometry.id_comp

added theorem AffineIsometry.id_toAffineMap

added theorem AffineIsometry.linear_eq_linearIsometry

added theorem AffineIsometry.map_eq_iff

added theorem AffineIsometry.map_ne

added theorem AffineIsometry.map_vadd

added theorem AffineIsometry.map_vsub

added theorem AffineIsometry.nndist_map

added theorem AffineIsometry.toAffineMap_injective

added structure AffineIsometry

added theorem AffineIsometryEquiv.apply_symm_apply

added theorem AffineIsometryEquiv.coe_constVadd

added theorem AffineIsometryEquiv.coe_constVsub

added theorem AffineIsometryEquiv.coe_inv

added theorem AffineIsometryEquiv.coe_mk'

added theorem AffineIsometryEquiv.coe_mk

added theorem AffineIsometryEquiv.coe_mul

added theorem AffineIsometryEquiv.coe_one

added theorem AffineIsometryEquiv.coe_refl

added theorem AffineIsometryEquiv.coe_symm_trans

added theorem AffineIsometryEquiv.coe_toAffineEquiv

added theorem AffineIsometryEquiv.coe_toAffineIsometry

added theorem AffineIsometryEquiv.coe_toHomeomorph

added theorem AffineIsometryEquiv.coe_toIsometryEquiv

added theorem AffineIsometryEquiv.coe_trans

added theorem AffineIsometryEquiv.coe_vaddConst'

added theorem AffineIsometryEquiv.coe_vaddConst

added theorem AffineIsometryEquiv.coe_vaddConst_symm

added theorem AffineIsometryEquiv.comp_continuousOn_iff

added theorem AffineIsometryEquiv.comp_continuous_iff

added def AffineIsometryEquiv.constVadd

added theorem AffineIsometryEquiv.constVadd_zero

added def AffineIsometryEquiv.constVsub

added theorem AffineIsometryEquiv.diam_image

added theorem AffineIsometryEquiv.dist_map

added theorem AffineIsometryEquiv.dist_pointReflection_fixed

added theorem AffineIsometryEquiv.dist_pointReflection_self'

added theorem AffineIsometryEquiv.dist_pointReflection_self

added theorem AffineIsometryEquiv.dist_pointReflection_self_real

added theorem AffineIsometryEquiv.ediam_image

added theorem AffineIsometryEquiv.edist_map

added theorem AffineIsometryEquiv.ext

added theorem AffineIsometryEquiv.linearIsometryEquiv_mk'

added theorem AffineIsometryEquiv.linear_eq_linear_isometry

added theorem AffineIsometryEquiv.map_eq_iff

added theorem AffineIsometryEquiv.map_ne

added theorem AffineIsometryEquiv.map_vadd

added theorem AffineIsometryEquiv.map_vsub

added def AffineIsometryEquiv.mk'

added def AffineIsometryEquiv.pointReflection

added theorem AffineIsometryEquiv.pointReflection_apply

added theorem AffineIsometryEquiv.pointReflection_fixed_iff

added theorem AffineIsometryEquiv.pointReflection_involutive

added theorem AffineIsometryEquiv.pointReflection_midpoint_left

added theorem AffineIsometryEquiv.pointReflection_midpoint_right

added theorem AffineIsometryEquiv.pointReflection_self

added theorem AffineIsometryEquiv.pointReflection_symm

added theorem AffineIsometryEquiv.pointReflection_toAffineEquiv

added theorem AffineIsometryEquiv.range_eq_univ

added def AffineIsometryEquiv.refl

added theorem AffineIsometryEquiv.refl_trans

added theorem AffineIsometryEquiv.self_trans_symm

added def AffineIsometryEquiv.symm

added theorem AffineIsometryEquiv.symm_apply_apply

added theorem AffineIsometryEquiv.symm_constVsub

added theorem AffineIsometryEquiv.symm_symm

added theorem AffineIsometryEquiv.symm_trans_self

added theorem AffineIsometryEquiv.toAffineEquiv_injective

added theorem AffineIsometryEquiv.toAffineEquiv_refl

added theorem AffineIsometryEquiv.toAffineEquiv_symm

added def AffineIsometryEquiv.toAffineIsometry

added def AffineIsometryEquiv.toHomeomorph

added theorem AffineIsometryEquiv.toHomeomorph_refl

added theorem AffineIsometryEquiv.toHomeomorph_symm

added def AffineIsometryEquiv.toIsometryEquiv

added theorem AffineIsometryEquiv.toIsometryEquiv_refl

added theorem AffineIsometryEquiv.toIsometryEquiv_symm

added def AffineIsometryEquiv.trans

added theorem AffineIsometryEquiv.trans_assoc

added theorem AffineIsometryEquiv.trans_refl

added def AffineIsometryEquiv.vaddConst

added theorem AffineIsometryEquiv.vaddConst_toAffineEquiv

added theorem AffineIsometryEquiv.vadd_vsub

added structure AffineIsometryEquiv

added theorem AffineMap.continuous_linear_iff

added theorem AffineMap.isOpenMap_linear_iff

added theorem AffineSubspace.coe_subtypeₐᵢ

added theorem AffineSubspace.isometryEquivMap.apply_symm_apply

added theorem AffineSubspace.isometryEquivMap.coe_apply

added theorem AffineSubspace.isometryEquivMap.toAffineMap_eq

added def AffineSubspace.subtypeₐᵢ

added theorem AffineSubspace.subtypeₐᵢ_linear

added theorem AffineSubspace.subtypeₐᵢ_linearIsometry

added theorem AffineSubspace.subtypeₐᵢ_toAffineMap

added theorem LinearIsometry.coe_toAffineIsometry

added def LinearIsometry.toAffineIsometry

added theorem LinearIsometry.toAffineIsometry_linearIsometry

added theorem LinearIsometry.toAffineIsometry_toAffineMap

added theorem LinearIsometryEquiv.coe_toAffineIsometryEquiv

added def LinearIsometryEquiv.toAffineIsometryEquiv

added theorem LinearIsometryEquiv.toAffineIsometryEquiv_linearIsometryEquiv

added theorem LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv

added theorem LinearIsometryEquiv.toAffineIsometryEquiv_toAffineIsometry