Commit 2024-04-08 10:17 cb4b5056

View on Github →

feat(Topology/Algebra/Module/StrongTopology): add monotonicity lemmas (#11600)

Estimated changes

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

added theorem UniformConvergenceCLM.topologicalSpace_eq

added theorem UniformConvergenceCLM.topologicalSpace_mono

modified theorem UniformConvergenceCLM.uniformEmbedding_coeFn

added theorem UniformConvergenceCLM.uniformSpace_eq

added theorem UniformConvergenceCLM.uniformSpace_mono