Commit 2024-10-05 23:41 3d9b4b5d

View on Github →

feat(StrongTopology): add lemmas about IsVonNBounded (#15217) Also add UniformOnFun.ofFun here and there to avoid type defeq abuse.

Estimated changes

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

added theorem ContinuousLinearMap.eventually_nhds_zero_mapsTo

added theorem ContinuousLinearMap.isVonNBounded_iff

added theorem ContinuousLinearMap.isVonNBounded_image2_apply

added theorem UniformConvergenceCLM.coe_zero

added theorem UniformConvergenceCLM.eventually_nhds_zero_mapsTo

added theorem UniformConvergenceCLM.isVonNBounded_iff

added theorem UniformConvergenceCLM.isVonNBounded_image2_apply

added theorem UniformConvergenceCLM.nhds_zero_eq

added theorem UniformConvergenceCLM.nhds_zero_eq_of_basis