Commit 2023-04-25 11:42 55212480

View on Github →

feat: port Analysis.NormedSpace.LinearIsometry (#3289)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/LinearIsometry.lean

added theorem Basis.ext_linearIsometry

added theorem Basis.ext_linearIsometryEquiv

added def LinearIsometry.Simps.apply

added theorem LinearIsometry.coe_comp

added theorem LinearIsometry.coe_id

added theorem LinearIsometry.coe_injective

added theorem LinearIsometry.coe_mk

added theorem LinearIsometry.coe_mul

added theorem LinearIsometry.coe_one

added theorem LinearIsometry.coe_toContinuousLinearMap

added theorem LinearIsometry.coe_toLinearMap

added def LinearIsometry.comp

added theorem LinearIsometry.comp_assoc

added theorem LinearIsometry.comp_continuous_iff

added theorem LinearIsometry.comp_id

added theorem LinearIsometry.diam_image

added theorem LinearIsometry.diam_range

added theorem LinearIsometry.dist_map

added theorem LinearIsometry.ediam_image

added theorem LinearIsometry.ediam_range

added theorem LinearIsometry.edist_map

added theorem LinearIsometry.ext

added def LinearIsometry.id

added theorem LinearIsometry.id_apply

added theorem LinearIsometry.id_comp

added theorem LinearIsometry.id_toContinuousLinearMap

added theorem LinearIsometry.id_toLinearMap

added theorem LinearIsometry.isComplete_image_iff

added theorem LinearIsometry.isComplete_map_iff'

added theorem LinearIsometry.isComplete_map_iff

added theorem LinearIsometry.map_eq_iff

added theorem LinearIsometry.map_ne

added theorem LinearIsometry.mul_def

added theorem LinearIsometry.nnnorm_map

added theorem LinearIsometry.norm_map

added theorem LinearIsometry.one_def

added theorem LinearIsometry.preimage_ball

added theorem LinearIsometry.preimage_closedBall

added theorem LinearIsometry.preimage_sphere

added def LinearIsometry.toContinuousLinearMap

added theorem LinearIsometry.toContinuousLinearMap_inj

added theorem LinearIsometry.toContinuousLinearMap_injective

added theorem LinearIsometry.toLinearMap_inj

added theorem LinearIsometry.toLinearMap_injective

added structure LinearIsometry

added def LinearIsometryEquiv.Simps.apply

added def LinearIsometryEquiv.Simps.symm_apply

added theorem LinearIsometryEquiv.apply_symm_apply

added theorem LinearIsometryEquiv.coe_coe''

added theorem LinearIsometryEquiv.coe_coe

added theorem LinearIsometryEquiv.coe_injective

added theorem LinearIsometryEquiv.coe_inv

added theorem LinearIsometryEquiv.coe_mk

added theorem LinearIsometryEquiv.coe_mul

added theorem LinearIsometryEquiv.coe_neg

added theorem LinearIsometryEquiv.coe_ofEq_apply

added theorem LinearIsometryEquiv.coe_ofLinearIsometry

added theorem LinearIsometryEquiv.coe_ofLinearIsometry_symm

added theorem LinearIsometryEquiv.coe_ofSurjective

added theorem LinearIsometryEquiv.coe_one

added theorem LinearIsometryEquiv.coe_prodAssoc

added theorem LinearIsometryEquiv.coe_prodAssoc_symm

added theorem LinearIsometryEquiv.coe_refl

added theorem LinearIsometryEquiv.coe_symm_trans

added theorem LinearIsometryEquiv.coe_toContinuousLinearEquiv

added theorem LinearIsometryEquiv.coe_toHomeomorph

added theorem LinearIsometryEquiv.coe_toIsometryEquiv

added theorem LinearIsometryEquiv.coe_toLinearEquiv

added theorem LinearIsometryEquiv.coe_toLinearIsometry

added theorem LinearIsometryEquiv.coe_trans

added theorem LinearIsometryEquiv.comp_continuousOn_iff

added theorem LinearIsometryEquiv.comp_continuous_iff

added theorem LinearIsometryEquiv.diam_image

added theorem LinearIsometryEquiv.dist_map

added theorem LinearIsometryEquiv.ediam_image

added theorem LinearIsometryEquiv.edist_map

added theorem LinearIsometryEquiv.ext

added theorem LinearIsometryEquiv.image_ball

added theorem LinearIsometryEquiv.image_closedBall

added theorem LinearIsometryEquiv.image_eq_preimage

added theorem LinearIsometryEquiv.image_sphere

added theorem LinearIsometryEquiv.inv_def

added theorem LinearIsometryEquiv.map_add

added theorem LinearIsometryEquiv.map_eq_iff

added theorem LinearIsometryEquiv.map_eq_zero_iff

added theorem LinearIsometryEquiv.map_ne

added theorem LinearIsometryEquiv.map_smul

added theorem LinearIsometryEquiv.map_smulₛₗ

added theorem LinearIsometryEquiv.map_sub

added theorem LinearIsometryEquiv.map_zero

added theorem LinearIsometryEquiv.mul_def

added theorem LinearIsometryEquiv.mul_refl

added def LinearIsometryEquiv.neg

added theorem LinearIsometryEquiv.nnnorm_map

added theorem LinearIsometryEquiv.norm_map

added def LinearIsometryEquiv.ofBounds

added def LinearIsometryEquiv.ofEq

added theorem LinearIsometryEquiv.ofEq_rfl

added theorem LinearIsometryEquiv.ofEq_symm

added def LinearIsometryEquiv.ofLinearIsometry

added def LinearIsometryEquiv.ofTop

added theorem LinearIsometryEquiv.one_def

added theorem LinearIsometryEquiv.one_trans

added theorem LinearIsometryEquiv.preimage_ball

added theorem LinearIsometryEquiv.preimage_closedBall

added theorem LinearIsometryEquiv.preimage_sphere

added def LinearIsometryEquiv.prodAssoc

added theorem LinearIsometryEquiv.range_eq_univ

added def LinearIsometryEquiv.refl

added theorem LinearIsometryEquiv.refl_mul

added theorem LinearIsometryEquiv.refl_trans

added theorem LinearIsometryEquiv.self_comp_symm

added theorem LinearIsometryEquiv.self_trans_symm

added def LinearIsometryEquiv.symm

added theorem LinearIsometryEquiv.symm_apply_apply

added theorem LinearIsometryEquiv.symm_comp_self

added theorem LinearIsometryEquiv.symm_neg

added theorem LinearIsometryEquiv.symm_symm

added theorem LinearIsometryEquiv.symm_trans

added theorem LinearIsometryEquiv.symm_trans_self

added def LinearIsometryEquiv.toContinuousLinearEquiv

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_inj

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_injective

added def LinearIsometryEquiv.toHomeomorph

added theorem LinearIsometryEquiv.toHomeomorph_inj

added theorem LinearIsometryEquiv.toHomeomorph_injective

added theorem LinearIsometryEquiv.toHomeomorph_symm

added def LinearIsometryEquiv.toIsometryEquiv

added theorem LinearIsometryEquiv.toIsometryEquiv_inj

added theorem LinearIsometryEquiv.toIsometryEquiv_injective

added theorem LinearIsometryEquiv.toIsometryEquiv_symm

added theorem LinearIsometryEquiv.toLinearEquiv_inj

added theorem LinearIsometryEquiv.toLinearEquiv_injective

added theorem LinearIsometryEquiv.toLinearEquiv_symm

added theorem LinearIsometryEquiv.toLinearEquiv_trans

added def LinearIsometryEquiv.toLinearIsometry

added theorem LinearIsometryEquiv.toLinearIsometry_inj

added theorem LinearIsometryEquiv.toLinearIsometry_injective

added def LinearIsometryEquiv.trans

added theorem LinearIsometryEquiv.trans_apply

added theorem LinearIsometryEquiv.trans_assoc

added theorem LinearIsometryEquiv.trans_one

added theorem LinearIsometryEquiv.trans_refl

added def LinearIsometryEquiv.ulift

added structure LinearIsometryEquiv

added def LinearMap.toLinearIsometry

added theorem SemilinearIsometryClass.diam_image

added theorem SemilinearIsometryClass.diam_range

added theorem SemilinearIsometryClass.ediam_image

added theorem SemilinearIsometryClass.ediam_range

added theorem SemilinearIsometryClass.nnnorm_map

added theorem Submodule.coe_subtypeₗᵢ

added def Submodule.subtypeₗᵢ

added theorem Submodule.subtypeₗᵢ_toContinuousLinearMap

added theorem Submodule.subtypeₗᵢ_toLinearMap