# mathlib3documentation

topology.instances.real

# Topological properties of ℝ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem real.mem_closure_iff {s : set } {x : } :
x (ε : ), ε > 0 ( (y : ) (H : y s), |y - x| < ε)
theorem real.uniform_continuous_inv (s : set ) {r : } (r0 : 0 < r) (H : (x : ), x s r |x|) :
theorem real.tendsto_inv {r : } (r0 : r 0) :
filter.tendsto (λ (q : ), q⁻¹) (nhds r) (nhds r⁻¹)
theorem real.continuous_inv  :
continuous (λ (a : {r // r 0}), (a.val)⁻¹)
theorem real.continuous.inv {α : Type u} {f : α } (h : (a : α), f a 0) (hf : continuous f) :
continuous (λ (a : α), (f a)⁻¹)
theorem real.uniform_continuous_mul (s : set ( × )) {r₁ r₂ : } (H : (x : × ), x s |x.fst| < r₁ |x.snd| < r₂) :
uniform_continuous (λ (p : s), p.val.fst * p.val.snd)
@[protected]
theorem real.continuous_mul  :
continuous (λ (p : × ), p.fst * p.snd)
@[protected, instance]
@[protected, instance]
theorem real.totally_bounded_ball (x ε : ) :
theorem closure_of_rat_image_lt {q : } :
closure (coe '' {x : | q < x}) = {r : | q r}
theorem function.periodic.compact_of_continuous' {α : Type u} {f : α} {c : } (hp : c) (hc : 0 < c) (hf : continuous f) :
theorem function.periodic.compact_of_continuous {α : Type u} {f : α} {c : } (hp : c) (hc : c 0) (hf : continuous f) :

A continuous, periodic function has compact range.

theorem function.periodic.bounded_of_continuous {α : Type u} {f : α} {c : } (hp : c) (hc : c 0) (hf : continuous f) :

A continuous, periodic function is bounded.

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

theorem int.tendsto_zmultiples_hom_cofinite {a : } (ha : a 0) :

For nonzero a, the "multiples of a" map zmultiples_hom 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.

theorem real.subgroup_dense_of_no_min {G : add_subgroup } {g₀ : } (g₀_in : g₀ G) (g₀_ne : g₀ 0) (H' : ¬ (a : ), is_least {g : | g G 0 < g} a) :

Given a nontrivial subgroup G ⊆ ℝ, if G ∩ ℝ_{>0} has no minimum then G is dense.

Subgroups of ℝ are either dense or cyclic. See real.subgroup_dense_of_no_min and subgroup_cyclic_of_min for more precise statements.