Commit 2023-04-27 14:06 4f8d8faf

View on Github →

feat: port Topology.Algebra.UniformConvergence (#3664)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/UniformConvergence.lean

added theorem UniformFun.div_apply

added theorem UniformFun.inv_apply

added theorem UniformFun.mul_apply

added theorem UniformFun.one_apply

added theorem UniformOnFun.continuousSMul_induced_of_image_bounded

added theorem UniformOnFun.continuousSMul_submodule_of_image_bounded

added theorem UniformOnFun.div_apply

added theorem UniformOnFun.inv_apply

added theorem UniformOnFun.mul_apply

added theorem UniformOnFun.one_apply