Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 12:08 c0f16d26

View on Github →

feat(analysis/normed_space/affine_isometry): new file, bundled affine isometries (#8660) This PR defines bundled affine isometries and affine isometry equivs, adapting the theory more or less wholesale from the linear isometry and affine map theories. In follow-up PRs I re-work the Mazur-Ulam and Euclidean geometry libraries to use these objects where appropriate.

Estimated changes

Modified docs/undergrad.yaml

Created src/analysis/normed_space/affine_isometry.lean

added theorem affine_isometry.coe_comp

added theorem affine_isometry.coe_fn_injective

added theorem affine_isometry.coe_id

added theorem affine_isometry.coe_mul

added theorem affine_isometry.coe_one

added theorem affine_isometry.coe_to_affine_isometry_equiv

added theorem affine_isometry.coe_to_affine_map

added def affine_isometry.comp

added theorem affine_isometry.comp_assoc

added theorem affine_isometry.comp_continuous_iff

added theorem affine_isometry.comp_id

added theorem affine_isometry.diam_image

added theorem affine_isometry.diam_range

added theorem affine_isometry.dist_map

added theorem affine_isometry.ediam_image

added theorem affine_isometry.ediam_range

added theorem affine_isometry.edist_map

added theorem affine_isometry.ext

added def affine_isometry.id

added theorem affine_isometry.id_apply

added theorem affine_isometry.id_comp

added theorem affine_isometry.id_to_affine_map

added theorem affine_isometry.linear_eq_linear_isometry

added theorem affine_isometry.map_eq_iff

added theorem affine_isometry.map_ne

added theorem affine_isometry.map_vadd

added theorem affine_isometry.map_vsub

added theorem affine_isometry.nndist_map

added theorem affine_isometry.to_affine_isometry_equiv_apply

added theorem affine_isometry.to_affine_map_injective

added structure affine_isometry

added theorem affine_isometry_equiv.apply_symm_apply

added theorem affine_isometry_equiv.coe_inv

added theorem affine_isometry_equiv.coe_mk'

added theorem affine_isometry_equiv.coe_mk

added theorem affine_isometry_equiv.coe_mul

added theorem affine_isometry_equiv.coe_one

added theorem affine_isometry_equiv.coe_refl

added theorem affine_isometry_equiv.coe_symm_trans

added theorem affine_isometry_equiv.coe_to_affine_equiv

added theorem affine_isometry_equiv.coe_to_affine_isometry

added theorem affine_isometry_equiv.coe_to_homeomorph

added theorem affine_isometry_equiv.coe_to_isometric

added theorem affine_isometry_equiv.coe_trans

added theorem affine_isometry_equiv.comp_continuous_iff

added theorem affine_isometry_equiv.comp_continuous_on_iff

added theorem affine_isometry_equiv.diam_image

added theorem affine_isometry_equiv.dist_map

added theorem affine_isometry_equiv.ediam_image

added theorem affine_isometry_equiv.edist_map

added theorem affine_isometry_equiv.ext

added theorem affine_isometry_equiv.linear_eq_linear_isometry

added theorem affine_isometry_equiv.linear_isometry_equiv_mk'

added theorem affine_isometry_equiv.map_eq_iff

added theorem affine_isometry_equiv.map_ne

added theorem affine_isometry_equiv.map_vadd

added theorem affine_isometry_equiv.map_vsub

added def affine_isometry_equiv.mk'

added theorem affine_isometry_equiv.range_eq_univ

added def affine_isometry_equiv.refl

added theorem affine_isometry_equiv.refl_trans

added def affine_isometry_equiv.symm

added theorem affine_isometry_equiv.symm_apply_apply

added theorem affine_isometry_equiv.symm_symm

added theorem affine_isometry_equiv.symm_trans

added theorem affine_isometry_equiv.to_affine_equiv_injective

added theorem affine_isometry_equiv.to_affine_equiv_refl

added theorem affine_isometry_equiv.to_affine_equiv_symm

added def affine_isometry_equiv.to_affine_isometry

added def affine_isometry_equiv.to_homeomorph

added theorem affine_isometry_equiv.to_homeomorph_refl

added theorem affine_isometry_equiv.to_homeomorph_symm

added def affine_isometry_equiv.to_isometric

added theorem affine_isometry_equiv.to_isometric_refl

added theorem affine_isometry_equiv.to_isometric_symm

added def affine_isometry_equiv.trans

added theorem affine_isometry_equiv.trans_assoc

added theorem affine_isometry_equiv.trans_refl

added theorem affine_isometry_equiv.trans_symm

added structure affine_isometry_equiv

added theorem linear_isometry.coe_to_affine_isometry

added def linear_isometry.to_affine_isometry

added theorem linear_isometry.to_affine_isometry_linear_isometry

added theorem linear_isometry.to_affine_isometry_to_affine_map

added theorem linear_isometry_equiv.coe_to_affine_isometry_equiv

added def linear_isometry_equiv.to_affine_isometry_equiv

added theorem linear_isometry_equiv.to_affine_isometry_equiv_linear_isometry_equiv

added theorem linear_isometry_equiv.to_affine_isometry_equiv_to_affine_equiv

added theorem linear_isometry_equiv.to_affine_isometry_equiv_to_affine_isometry

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry.id_apply

added theorem linear_isometry.id_to_linear_map

deleted theorem linear_isometry_equiv.linear_isometry.id_apply

deleted theorem linear_isometry_equiv.linear_isometry.id_to_linear_map

Modified src/linear_algebra/affine_space/affine_equiv.lean

modified def affine_equiv.mk'

deleted theorem affine_equiv.to_equiv_mk'