mathlib documentation

topology.instances.real

Topological properties of ℝ

source
@[instance]
def rat.metric_space  :
metric_space ℚ

Equations
source
theorem rat.dist_eq (x y : ℚ) :
dist x y = abs (↑x - ↑y)

source
@[simp]
theorem rat.dist_cast (x y : ℚ) :
dist ↑x ↑y = dist x y

source
@[instance]
def int.metric_space  :
metric_space ℤ

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

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

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

source
theorem uniform_continuous_of_rat  :
uniform_continuous coe

source
theorem uniform_embedding_of_rat  :
uniform_embedding coe

source
theorem dense_embedding_of_rat  :
dense_embedding coe

source
theorem embedding_of_rat  :
embedding coe

source
theorem continuous_of_rat  :
continuous coe

source
theorem real.uniform_continuous_add  :
uniform_continuous (λ (p : ℝ × ℝ), p.fst + p.snd)

source
theorem rat.uniform_continuous_add  :
uniform_continuous (λ (p : ℚ × ℚ), p.fst + p.snd)

source
theorem real.uniform_continuous_neg  :
uniform_continuous has_neg.neg

source
theorem rat.uniform_continuous_neg  :
uniform_continuous has_neg.neg

source
@[instance]
def real.uniform_add_group  :
uniform_add_group ℝ

source
@[instance]
def rat.uniform_add_group  :
uniform_add_group ℚ

source
@[instance]
def real.topological_add_group  :
topological_add_group ℝ

source
@[instance]
def rat.topological_add_group  :
topological_add_group ℚ

source
@[instance]
def rat.order_topology  :
order_topology ℚ

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

source
@[instance]
def real.topological_space.second_countable_topology  :
topological_space.second_countable_topology ℝ

source
theorem real.uniform_continuous_inv (s : set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ (x : ℝ), x ∈ s → r ≤ abs x) :
uniform_continuous (λ (p : ↥s), (p.val)⁻¹)

source
theorem real.uniform_continuous_abs  :
uniform_continuous abs

source
theorem real.continuous_abs  :
continuous abs

source
theorem rat.uniform_continuous_abs  :
uniform_continuous abs

source
theorem rat.continuous_abs  :
continuous abs

source
theorem real.tendsto_inv {r : ℝ} (r0 : r ≠ 0) :
(λ (q : ℝ), q⁻¹)→_{r}r⁻¹

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

source
theorem real.continuous.inv {α : Type u} [topological_space α] {f : α → ℝ} (h : ∀ (a : α), f a ≠ 0) (hf : continuous f) :
continuous (λ (a : α), (f a)⁻¹)

source
theorem real.uniform_continuous_mul_const {x : ℝ} :
uniform_continuous (has_mul.mul x)

source
theorem real.uniform_continuous_mul (s : set (ℝ × ℝ)) {r₁ r₂ : ℝ} (H : ∀ (x : ℝ × ℝ), x ∈ s → abs x.fst < r₁ ∧ abs x.snd < r₂) :
uniform_continuous (λ (p : ↥s), (p.val.fst) * p.val.snd)

source
theorem real.continuous_mul  :
continuous (λ (p : ℝ × ℝ), (p.fst) * p.snd)

source
@[instance]
def real.topological_ring  :
topological_ring ℝ

source
@[instance]
def real.topological_semiring  :
topological_semiring ℝ

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

source
@[instance]
def rat.topological_ring  :
topological_ring ℚ

source
theorem real.ball_eq_Ioo (x ε : ℝ) :
metric.ball x ε = set.Ioo (x - ε) (x + ε)

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

source
theorem real.totally_bounded_Ioo (a b : ℝ) :
totally_bounded (set.Ioo a b)

source
theorem real.totally_bounded_ball (x ε : ℝ) :
totally_bounded (metric.ball x ε)

source
theorem real.totally_bounded_Ico (a b : ℝ) :
totally_bounded (set.Ico a b)

source
theorem real.totally_bounded_Icc (a b : ℝ) :
totally_bounded (set.Icc a b)

source
theorem rat.totally_bounded_Icc (a b : ℚ) :
totally_bounded (set.Icc a b)

source
@[instance]
def real.complete_space  :
complete_space ℝ

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

source
theorem compact_Icc {a b : ℝ} :
is_compact (set.Icc a b)

source
@[instance]
def real.proper_space  :
proper_space ℝ

source
theorem real.bounded_iff_bdd_below_bdd_above {s : set ℝ} :
metric.bounded s ↔ bdd_below s ∧ bdd_above s

source
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))