Topological properties of ℝ

theorem Real.isTopologicalBasis_Ioo_rat : TopologicalSpace.IsTopologicalBasis (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

@[simp]

theorem Real.cobounded_eq : Bornology.cobounded ℝ = Filter.atBot ⊔ Filter.atTop

theorem Real.mem_closure_iff {s : Set ℝ} {x : ℝ} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

theorem Real.uniformContinuous_inv (s : Set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ |x|) : UniformContinuous fun (p : ↑s) => (↑p)⁻¹

theorem Real.uniformContinuous_abs : UniformContinuous abs

theorem Real.continuous_inv : Continuous fun (a : { r : ℝ // r ≠ 0 }) => (↑a)⁻¹

theorem Real.uniformContinuous_mul (s : Set (ℝ × ℝ)) {r₁ r₂ : ℝ} (H : ∀ x ∈ s, |x.1| < r₁ ∧ |x.2| < r₂) : UniformContinuous fun (p : ↑s) => (↑p).1 * (↑p).2

theorem Real.totallyBounded_ball (x ε : ℝ) : TotallyBounded (Metric.ball x ε)

theorem Real.subfield_eq_of_closed {K : Subfield ℝ} (hc : IsClosed ↑K) : K = ⊤

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 closure_ordConnected_inter_rat {s : Set ℝ} (conn : s.OrdConnected) (nt : s.Nontrivial) : closure (s ∩ Set.range Rat.cast) = closure s

theorem closure_of_rat_image_lt {q : ℚ} : closure (Rat.cast '' {x : ℚ | q < x}) = {r : ℝ | ↑q ≤ r}

theorem Function.Periodic.compact_of_continuous {α : Type u} [TopologicalSpace α] {f : ℝ → α} {c : ℝ} (hp : Periodic f c) (hc : c ≠ 0) (hf : Continuous f) : IsCompact (Set.range 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) : Bornology.IsBounded (Set.range f)

A continuous, periodic function is bounded.