mathlib

4416eacb - feat(topology/instances/real): a continuous periodic function has compact range (and is hence bounded) (#7968)

feat(topology/instances/real): a continuous periodic function has compact range (and is hence bounded) (#7968) A few more facts about periodic functions, namely: - If a function `f` is `periodic` with positive period `p`, then for all `x` there exists `y` such that `y` is an element of `[0, p)` and `f x = f y` - A continuous, periodic function has compact range - A continuous, periodic function is bounded