mathlib3 documentation

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]

def real.noncompact_space :

noncompact_space ℝ

theorem real.uniform_continuous_add :

uniform_continuous (λ (p : ℝ × ℝ), p.fst + p.snd)

theorem real.uniform_continuous_neg :

uniform_continuous has_neg.neg

@[protected, instance]

def real.has_continuous_star :

has_continuous_star ℝ

@[protected, instance]

def real.uniform_add_group :

uniform_add_group ℝ

@[protected, instance]

def real.topological_add_group :

topological_add_group ℝ

@[protected, instance]

def real.proper_space :

proper_space ℝ

@[protected, instance]

def real.topological_space.second_countable_topology :

topological_space.second_countable_topology ℝ

theorem real.is_topological_basis_Ioo_rat :

topological_space.is_topological_basis (⋃ (a b : ℚ) (h : a < b), {set.Ioo ↑a ↑b})

@[simp]

theorem real.cocompact_eq :

filter.cocompact ℝ = filter.at_bot ⊔ filter.at_top

theorem real.mem_closure_iff {s : set ℝ} {x : ℝ} :

x ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (y : ℝ) (H : y ∈ s), |y - x| < ε)

theorem real.uniform_continuous_inv (s : set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ (x : ℝ), x ∈ s → r ≤ |x|) :

uniform_continuous (λ (p : ↥s), (p.val)⁻¹)

theorem real.uniform_continuous_abs :

uniform_continuous has_abs.abs

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} [topological_space α] {f : α → ℝ} (h : ∀ (a : α), f a ≠ 0) (hf : continuous f) :

continuous (λ (a : α), (f a)⁻¹)

theorem real.uniform_continuous_const_mul {x : ℝ} :

uniform_continuous (has_mul.mul x)

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]

def real.topological_ring :

topological_ring ℝ

@[protected, instance]

def real.complete_space :

complete_space ℝ

theorem real.totally_bounded_ball (x ε : ℝ) :

totally_bounded (metric.ball x ε)

theorem closure_of_rat_image_lt {q : ℚ} :

closure (coe '' {x : ℚ | q < x}) = {r : ℝ | ↑q ≤ r}

theorem real.bounded_iff_bdd_below_bdd_above {s : set ℝ} :

metric.bounded s ↔ bdd_below s ∧ bdd_above s

theorem real.subset_Icc_Inf_Sup_of_bounded {s : set ℝ} (h : metric.bounded s) :

s ⊆ set.Icc (has_Inf.Inf s) (has_Sup.Sup s)

theorem function.periodic.compact_of_continuous' {α : Type u} [topological_space α] {f : ℝ → α} {c : ℝ} (hp : function.periodic f c) (hc : 0 < c) (hf : continuous f) :

is_compact (set.range f)

theorem function.periodic.compact_of_continuous {α : Type u} [topological_space α] {f : ℝ → α} {c : ℝ} (hp : function.periodic f c) (hc : c ≠ 0) (hf : continuous f) :

is_compact (set.range f)

A continuous, periodic function has compact range.

theorem function.periodic.bounded_of_continuous {α : Type u} [pseudo_metric_space α] {f : ℝ → α} {c : ℝ} (hp : function.periodic f c) (hc : c ≠ 0) (hf : continuous f) :

metric.bounded (set.range f)

A continuous, periodic function is bounded.

theorem int.tendsto_coe_cofinite :

filter.tendsto coe filter.cofinite (filter.cocompact ℝ)

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

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

filter.tendsto ⇑(⇑(zmultiples_hom ℝ) a) filter.cofinite (filter.cocompact ℝ)

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

theorem add_subgroup.tendsto_zmultiples_subtype_cofinite (a : ℝ) :

filter.tendsto ⇑((add_subgroup.zmultiples a).subtype) filter.cofinite (filter.cocompact ℝ)

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.

theorem real.subgroup_dense_or_cyclic (G : add_subgroup ℝ) :

dense ↑G ∨ ∃ (a : ℝ), G = add_subgroup.closure {a}

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