Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.periodic.compact_of_continuous

Modification history

2021-06-22 03:06
src/topology/instances/real.lean
feat(topology/instances/real): a continuous periodic function has compact range (and is hence bounded) (#7968) …
Added function.periodic.compact_of_continuousView on Github →