# Topological properties of ℝ #

Equations
theorem Real.isTopologicalBasis_Ioo_rat :
TopologicalSpace.IsTopologicalBasis (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})
@[simp]
theorem Real.cobounded_eq :
= Filter.atBot Filter.atTop
@[deprecated cocompact_eq_atBot_atTop]
theorem Real.cocompact_eq {α : Type u_2} [] [] [] [] [] :
= Filter.atBot Filter.atTop

Alias of cocompact_eq_atBot_atTop.

@[deprecated atBot_le_cocompact]
theorem Real.atBot_le_cocompact {α : Type u_2} [] [] [] :
Filter.atBot

Alias of atBot_le_cocompact.

@[deprecated atTop_le_cocompact]
theorem Real.atTop_le_cocompact {α : Type u_2} [] [] [] :
Filter.atTop

Alias of atTop_le_cocompact.

theorem Real.mem_closure_iff {s : } {x : } :
x ε > 0, ∃ y ∈ s, |y - x| < ε
theorem Real.uniformContinuous_inv (s : ) {r : } (r0 : 0 < r) (H : xs, r |x|) :
UniformContinuous fun (p : s) => (p)⁻¹
@[deprecated HasContinuousInv₀.continuousAt_inv₀]
theorem Real.tendsto_inv {r : } (r0 : r 0) :
Filter.Tendsto (fun (q : ) => q⁻¹) (nhds r) ()
theorem Real.continuous_inv :
Continuous fun (a : { r : // r 0 }) => (a)⁻¹
@[deprecated Continuous.inv₀]
theorem Real.Continuous.inv {α : Type u} [] {f : α} (h : ∀ (a : α), f a 0) (hf : ) :
Continuous fun (a : α) => (f a)⁻¹
theorem Real.uniformContinuous_mul (s : Set ()) {r₁ : } {r₂ : } (H : xs, |x.1| < r₁ |x.2| < r₂) :
UniformContinuous fun (p : s) => (p).1 * (p).2
@[deprecated continuous_mul]
theorem Real.continuous_mul :
Continuous fun (p : ) => p.1 * p.2
theorem Real.totallyBounded_ball (x : ) (ε : ) :
theorem closure_of_rat_image_lt {q : } :
closure (Rat.cast '' {x : | q < x}) = {r : | q r}
theorem Function.Periodic.compact_of_continuous {α : Type u} [] {f : α} {c : } (hp : ) (hc : c 0) (hf : ) :

A continuous, periodic function has compact range.

@[deprecated Function.Periodic.compact_of_continuous]
theorem Function.Periodic.compact_of_continuous' {α : Type u} [] {f : α} {c : } (hp : ) (hc : 0 < c) (hf : ) :
theorem Function.Periodic.isBounded_of_continuous {α : Type u} {f : α} {c : } (hp : ) (hc : c 0) (hf : ) :

A continuous, periodic function is bounded.

This is a special case of NormedSpace.discreteTopology_zmultiples. It exists only to simplify dependencies.

Equations
• =
theorem Int.tendsto_coe_cofinite :
Filter.Tendsto Int.cast Filter.cofinite

Under the coercion from ℤ to ℝ, inverse images of compact sets are finite.

theorem Int.tendsto_zmultiplesHom_cofinite {a : } (ha : a 0) :
Filter.Tendsto (( a)) Filter.cofinite

For nonzero a, the "multiples of a" map zmultiplesHom from ℤ to ℝ is discrete, i.e. inverse images of compact sets are finite.

The subgroup "multiples of a" (zmultiples a) is a discrete subgroup of ℝ, i.e. its intersection with compact sets is finite.