uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence (#14693)

Commit

3 years ago

feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence (#14693)

Author

ADedecker

Parents

e1452ef2

mathlib 11878a45 - feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence (#14693)

mathlib
11878a45 - feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence (#14693)