mathlib documentation

topology.instances.real

Topological properties of ℝ #

@[instance]
Equations
theorem rat.dist_eq (x y : ) :
dist x y = abs (x - y)
@[simp]
theorem rat.dist_cast (x y : ) :
dist x y = dist x y
theorem int.dist_eq (x y : ) :
dist x y = abs (x - y)
@[simp]
theorem int.dist_cast_real (x y : ) :
dist x y = dist x y
@[simp]
theorem int.dist_cast_rat (x y : ) :
dist x y = dist x y
theorem int.ball_eq (x : ) (r : ) :
@[instance]
theorem real.mem_closure_iff {s : set } {x : } :
x closure s ∀ (ε : ), ε > 0(∃ (y : ) (H : y s), abs (y - x) < ε)
theorem real.uniform_continuous_inv (s : set ) {r : } (r0 : 0 < r) (H : ∀ (x : ), x sr abs x) :
theorem real.tendsto_inv {r : } (r0 : r 0) :
filter.tendsto (λ (q : ), q⁻¹) (𝓝 r) (𝓝 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_mul (s : set ( × )) {r₁ r₂ : } (H : ∀ (x : × ), x sabs x.fst < r₁ abs x.snd < r₂) :
uniform_continuous (λ (p : s), (p.val.fst) * p.val.snd)
theorem real.continuous_mul  :
continuous (λ (p : × ), (p.fst) * p.snd)
theorem rat.continuous_mul  :
continuous (λ (p : × ), (p.fst) * p.snd)
theorem real.ball_eq_Ioo (x ε : ) :
metric.ball x ε = set.Ioo (x - ε) (x + ε)
theorem real.Ioo_eq_ball (x y : ) :
set.Ioo x y = metric.ball ((x + y) / 2) ((y - x) / 2)
theorem closure_of_rat_image_lt {q : } :
closure (coe '' {x : | q < x}) = {r : | q r}
theorem real.image_Icc {f : } {a b : } (hab : a b) (h : continuous_on f (set.Icc a b)) :
f '' set.Icc a b = set.Icc (Inf (f '' set.Icc a b)) (Sup (f '' set.Icc a b))
theorem real.image_interval_eq_Icc {f : } {a b : } (h : continuous_on f [a, b]) :
f '' [a, b] = set.Icc (Inf (f '' [a, b])) (Sup (f '' [a, b]))
theorem real.image_interval {f : } {a b : } (h : continuous_on f [a, b]) :
f '' [a, b] = [Inf (f '' [a, b]), Sup (f '' [a, b])]
theorem real.interval_subset_image_interval {f : } {a b x y : } (h : continuous_on f [a, b]) (hx : x [a, b]) (hy : y [a, b]) :
[f x, f y] f '' [a, b]
theorem function.periodic.compact_of_continuous' {α : Type u} [topological_space α] {f : → α} {c : } (hp : function.periodic f c) (hc : 0 < c) (hf : continuous f) :
theorem function.periodic.compact_of_continuous {α : Type u} [topological_space α] {f : → α} {c : } (hp : function.periodic f c) (hc : c 0) (hf : continuous 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) :

A continuous, periodic function is bounded.

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.