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.

theorem Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici {f : ℕ → ℝ} {k : ℕ} (h_mon : MonotoneOn f (Set.Ici k)) (h_bdd : BddAbove (f '' Set.Ici k)) : Filter.Tendsto f Filter.atTop (nhds (sSup (f '' Set.Ici k)))

A monotone, bounded above sequence f : ℕ → ℝ on Ici k has the finite limit sSup (f '' Ici k).

theorem Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici {f : ℕ → ℝ} {k : ℕ} (h_ant : AntitoneOn f (Set.Ici k)) (h_bdd : BddBelow (f '' Set.Ici k)) : Filter.Tendsto f Filter.atTop (nhds (sInf (f '' Set.Ici k)))

An antitone, bounded below sequence f : ℕ → ℝ on Ici k has the finite limit sInf (f '' Ici k).

theorem Real.isLUB_of_tendsto_monotone_bddAbove {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {f : ι → ℝ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_mon : Monotone f) (h_bdd : BddAbove (Set.range f)) : IsLUB (Set.range f) x

The limit of a monotone, bounded above function f : ι → ℝ is a least upper bound of the function.

theorem Real.isGLB_of_tendsto_antitone_bddBelow {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {f : ι → ℝ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_ant : Antitone f) (h_bdd : BddBelow (Set.range f)) : IsGLB (Set.range f) x

The limit of an antitone, bounded below function f : ι → ℝ is a greatest lower bound of the function.

theorem Real.isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici {f : ℕ → ℝ} {k : ℕ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_mon : MonotoneOn f (Set.Ici k)) (h_bdd : BddAbove (f '' Set.Ici k)) : IsLUB (f '' Set.Ici k) x

The limit of an antitone, bounded below sequence f : ℕ → ℝ on Ici k is a least upper bound of the sequence.

theorem Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici {f : ℕ → ℝ} {k : ℕ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_ant : AntitoneOn f (Set.Ici k)) (h_bdd : BddBelow (f '' Set.Ici k)) : IsGLB (f '' Set.Ici k) x

The limit of an antitone, bounded below sequence f : ℕ → ℝ on Ici k is a greatest lower bound of the sequence.