compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292)

Commit

3 years ago

feat(topology/uniform_space/compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292) Also, locally uniform convergence is just uniform convergence when the domain is compact.

Author

ocfnash

Parents

20997252

mathlib3 deac58aa - feat(topology/uniform_space/compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292)

mathlib3
deac58aa - feat(topology/uniform_space/compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292)