Theorem ContinuousLinearMap.uniformEmbedding_toUniformOnFun

Modification history

2024-10-03 20:47

Mathlib/Topology/Algebra/Module/StrongTopology.lean

chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) …

Deleted ContinuousLinearMap.uniformEmbedding_toUniformOnFun View on Github →

2024-08-12 20:23

Mathlib/Topology/Algebra/Module/StrongTopology.lean

feat(StrongTopology): generalize `ContinuousLinearMap.restrictScalarsL` (#15285)

Added ContinuousLinearMap.uniformEmbedding_toUniformOnFun View on Github →