Commit 2023-05-12 16:00 1fb5eb7e

View on Github →

feat: port Analysis.LocallyConvex.ContinuousOfBounded (#3944)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean

added def LinearMap.clmOfExistsBoundedImage

added theorem LinearMap.clmOfExistsBoundedImage_apply

added theorem LinearMap.clmOfExistsBoundedImage_coe

added theorem LinearMap.continuousAt_zero_of_locally_bounded

added theorem LinearMap.continuous_of_locally_bounded