# mathlibdocumentation

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 : ) :
y = dist x y

@[instance]

Equations
theorem int.dist_eq (x y : ) :
dist x y = abs (x - y)

@[simp]
theorem int.dist_cast_real (x y : ) :
y = dist x y

@[simp]
theorem int.dist_cast_rat (x y : ) :
y = dist x y

theorem embedding_of_rat  :

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

theorem real.mem_closure_iff {s : set } {x : } :
x ∀ (ε : ), ε > 0(∃ (y : ) (H : y s), abs (y - x) < ε)

theorem real.uniform_continuous_inv (s : set ) {r : } :
0 < r(∀ (x : ), x sr abs x)uniform_continuous (λ (p : s), (p.val)⁻¹)

theorem real.tendsto_inv {r : } :
r 0filter.tendsto (λ (q : ), q⁻¹) (𝓝 r) (𝓝 r⁻¹)

theorem real.continuous_inv  :
continuous (λ (a : {r // r 0}), (a.val)⁻¹)

theorem real.continuous.inv {α : Type u} {f : α → } :
(∀ (a : α), f a 0)continuous (λ (a : α), (f a)⁻¹)

theorem real.uniform_continuous_mul (s : set ( × )) {r₁ r₂ : } :
(∀ (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)

@[instance]

@[instance]

theorem rat.continuous_mul  :
continuous (λ (p : × ), (p.fst) * p.snd)

@[instance]

theorem real.ball_eq_Ioo (x ε : ) :
ε = set.Ioo (x - ε) (x + ε)

theorem real.Ioo_eq_ball (x y : ) :
y = metric.ball ((x + y) / 2) ((y - x) / 2)

theorem real.totally_bounded_ball (x ε : ) :

@[instance]

theorem closure_of_rat_image_lt {q : } :
closure (coe '' {x : | q < x}) = {r : | q r}

theorem compact_Icc {a b : } :

@[instance]

theorem real.image_Icc {f : } {a b : } :
a b (set.Icc a b)f '' b = set.Icc (Inf (f '' b)) (Sup (f '' b))

@[instance]

@[instance]
def real_maps_algebra {α : Type u_1}  :

Equations
theorem real.subgroup_dense_of_no_min {G : add_subgroup } {g₀ : } :
g₀ Gg₀ 0(¬∃ (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 ) :
∃ (a : ),

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