Commit 2023-04-12 19:26 4472bdb6

View on Github →

feat: port Analysis.NormedSpace.ContinuousLinearMap (#3381)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

added theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm

added theorem ContinuousLinearEquiv.coord_self

added theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton

added theorem ContinuousLinearEquiv.homothety_inverse

added theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord

added theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety

added theorem ContinuousLinearMap.antilipschitz_of_bound

added theorem ContinuousLinearMap.bound_of_antilipschitz

added def ContinuousLinearMap.ofHomothety

added def ContinuousLinearMap.toSpanSingleton

added theorem ContinuousLinearMap.toSpanSingleton_add

added theorem ContinuousLinearMap.toSpanSingleton_apply

added theorem ContinuousLinearMap.toSpanSingleton_homothety

added theorem ContinuousLinearMap.toSpanSingleton_smul'

added theorem ContinuousLinearMap.toSpanSingleton_smul

added theorem ContinuousLinearMap.uniformEmbedding_of_bound

added def LinearEquiv.toContinuousLinearEquivOfBounds

added def LinearMap.mkContinuous

added def LinearMap.mkContinuousOfExistsBound

added theorem LinearMap.mkContinuousOfExistsBound_apply

added theorem LinearMap.mkContinuousOfExistsBound_coe

added theorem LinearMap.mkContinuous_apply

added theorem LinearMap.mkContinuous_coe

added def LinearMap.toContinuousLinearMap₁

added theorem LinearMap.toContinuousLinearMap₁_apply

added theorem LinearMap.toContinuousLinearMap₁_coe

added theorem continuous_of_linear_of_bound

added theorem continuous_of_linear_of_boundₛₗ