isBounded_of_continuous — Mathlib

English

A continuous, periodic function is bounded (on its range).

Русский

Непрерывная периодическая функция ограничена по значению на своем образе.

LaTeX

$$$\text{IsBounded}(\operatorname{range}f)$ for periodic $f$ that is continuous$$

Lean4

/-- A continuous, periodic function is bounded. -/
theorem isBounded_of_continuous [PseudoMetricSpace α] {f : ℝ → α} {c : ℝ} (hp : Periodic f c) (hc : c ≠ 0)
    (hf : Continuous f) : IsBounded (range f) :=
  (hp.compact_of_continuous hc hf).isBounded

Похожие утверждения