mathlib docs: topology.instances.real

source

@[instance]

def rat.metric_space :

metric_space ℚ

Equations

rat.metric_space = metric_space.induced coe rat.metric_space._proof_1 real.metric_space

source

theorem rat.dist_eq (x y : ℚ) :

has_dist.dist x y = abs (↑x - ↑y)

source

@[simp]

theorem rat.dist_cast (x y : ℚ) :

has_dist.dist ↑x ↑y = has_dist.dist x y

source

@[instance]

def int.metric_space :

metric_space ℤ

Equations

int.metric_space = let M : metric_space ℤ := metric_space.induced coe int.metric_space._proof_1 real.metric_space in M.replace_uniformity int.metric_space._proof_2

source

theorem int.dist_eq (x y : ℤ) :

has_dist.dist x y = abs (↑x - ↑y)

source

@[simp]

theorem int.dist_cast_real (x y : ℤ) :

has_dist.dist ↑x ↑y = has_dist.dist x y

source

@[simp]

theorem int.dist_cast_rat (x y : ℤ) :

has_dist.dist ↑x ↑y = has_dist.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 ℝ

Equations

real.uniform_add_group = _

source

@[instance]

def rat.uniform_add_group :

uniform_add_group ℚ

Equations

rat.uniform_add_group = _

source

@[instance]

def real.topological_add_group :

topological_add_group ℝ

Equations

real.topological_add_group = uniform_add_group.to_topological_add_group

source

@[instance]

def rat.topological_add_group :

topological_add_group ℚ

Equations

rat.topological_add_group = uniform_add_group.to_topological_add_group

source

@[instance]

def rat.order_topology :

order_topology ℚ

Equations

rat.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 ℝ

Equations

real.topological_space.second_countable_topology = _

source

theorem real.uniform_continuous_inv (s : set ℝ) {r : ℝ} :

0 < r → (∀ (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 : ℝ} :

r ≠ 0 → filter.tendsto (λ (q : ℝ), q⁻¹) (nhds r) (nhds r⁻¹)

source

theorem real.continuous_inv :

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

source

theorem real.continuous.inv {α : Type u} [topological_space α] {f : α → ℝ} :

(∀ (a : α), f a ≠ 0) → 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₂ : ℝ} :

(∀ (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 ℝ

Equations

real.topological_ring = _

source

@[instance]

def real.topological_semiring :

topological_semiring ℝ

Equations

real.topological_semiring = _

source

theorem rat.continuous_mul :

continuous (λ (p : ℚ × ℚ), p.fst * p.snd)

source

@[instance]

def rat.topological_ring :

topological_ring ℚ

Equations

rat.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 ℝ

Equations

real.complete_space = _

source

theorem tendsto_coe_nat_real_at_top_iff {α : Type u} {f : α → ℕ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top

source

theorem tendsto_coe_nat_real_at_top_at_top :

filter.tendsto coe filter.at_top filter.at_top

source

theorem tendsto_coe_int_real_at_top_iff {α : Type u} {f : α → ℤ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top

source

theorem tendsto_coe_int_real_at_top_at_top :

filter.tendsto coe filter.at_top filter.at_top

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 ℝ

Equations

real.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 : ℝ} :

a ≤ b → continuous_on f (set.Icc a b) → f '' set.Icc a b = set.Icc (has_Inf.Inf (f '' set.Icc a b)) (has_Sup.Sup (f '' set.Icc a b))

mathlib documentation

topology.instances.real

Topological properties of ℝ

General documentation

Additional documentation

Library

mathlib documentation

topology.​instances.​real

Topological properties of ℝ

General documentation

Additional documentation

Library

topology.instances.real