# Documentation

Mathlib.Topology.Instances.Real

# Topological properties of ℝ #

@[simp]
theorem Real.cocompact_eq :
= Filter.atBot Filter.atTop
theorem Real.mem_closure_iff {s : } {x : } :
x ∀ (ε : ), ε > 0y, y s |y - x| < ε
theorem Real.uniformContinuous_inv (s : ) {r : } (r0 : 0 < r) (H : ∀ (x : ), x sr |x|) :
UniformContinuous fun p => (p)⁻¹
@[deprecated HasContinuousInv₀.continuousAt_inv₀]
theorem Real.tendsto_inv {r : } (r0 : r 0) :
Filter.Tendsto (fun q => q⁻¹) (nhds r) ()
@[deprecated Continuous.inv₀]
theorem Real.Continuous.inv {α : Type u} [] {f : α} (h : ∀ (a : α), f a 0) (hf : ) :
Continuous fun a => (f a)⁻¹
theorem Real.uniformContinuous_const_mul {x : } :
UniformContinuous ((fun x x_1 => x * x_1) x)
theorem Real.uniformContinuous_mul (s : Set ()) {r₁ : } {r₂ : } (H : ∀ (x : ), x s|x.fst| < r₁ |x.snd| < r₂) :
UniformContinuous fun p => (p).fst * (p).snd
@[deprecated continuous_mul]
theorem Real.continuous_mul :
Continuous fun p => p.fst * p.snd
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.

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.