Theorem ContinuousMultilinearMap.range_toUniformOnFun

Modification history

2024-07-01 13:36

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

feat: generalize `CompleteSpace (ContinuousMultilinearMap _ _ _)` to TVS (#13468)

Added ContinuousMultilinearMap.range_toUniformOnFun View on Github →