Topological properties of ℝ #
theorem
Real.exists_seq_rat_strictMono_tendsto
(x : ℝ)
:
∃ (u : ℕ → ℚ), StrictMono u ∧ (∀ (n : ℕ), ↑(u n) < x) ∧ Filter.Tendsto (fun (x : ℕ) => ↑(u x)) Filter.atTop (nhds x)
theorem
Real.exists_seq_rat_strictAnti_tendsto
(x : ℝ)
:
∃ (u : ℕ → ℚ), StrictAnti u ∧ (∀ (n : ℕ), x < ↑(u n)) ∧ Filter.Tendsto (fun (x : ℕ) => ↑(u x)) Filter.atTop (nhds x)
theorem
Function.Periodic.compact_of_continuous
{α : Type u}
[TopologicalSpace α]
{f : ℝ → α}
{c : ℝ}
(hp : Periodic f c)
(hc : c ≠ 0)
(hf : Continuous f)
:
A continuous, periodic function has compact range.
theorem
Function.Periodic.isBounded_of_continuous
{α : Type u}
[PseudoMetricSpace α]
{f : ℝ → α}
{c : ℝ}
(hp : Periodic f c)
(hc : c ≠ 0)
(hf : Continuous f)
:
A continuous, periodic function is bounded.