Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.periodic.exists_mem_Ico

Modification history

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