Commit 2024-07-01 13:36 050f5a8d

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

added theorem Filter.Tendsto.isVonNBounded_range

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

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

added theorem ContinuousMultilinearMap.completeSpace

added theorem ContinuousMultilinearMap.range_toUniformOnFun

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

added theorem UniformOnFun.uniformContinuous_eval