Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousLinearMap.isUniformEmbedding_of_bound
Modification history
2024-10-03 20:47
Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean
chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) …
Added
ContinuousLinearMap.isUniformEmbedding_of_bound
View on Github →