Topology on the ratonal numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The structure of a metric space on ℚ is introduced in this file, induced from ℝ.

source

@[protected, 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 = |↑x - ↑y|

source

@[simp, norm_cast]

theorem rat.dist_cast (x y : ℚ) :

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

source

theorem rat.uniform_continuous_coe_real :

uniform_continuous coe

source

theorem rat.uniform_embedding_coe_real :

uniform_embedding coe

source

theorem rat.dense_embedding_coe_real :

dense_embedding coe

source

theorem rat.embedding_coe_real :

embedding coe

source

theorem rat.continuous_coe_real :

continuous coe

source

@[simp, norm_cast]

theorem nat.dist_cast_rat (x y : ℕ) :

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

source

theorem nat.uniform_embedding_coe_rat :

uniform_embedding coe

source

theorem nat.closed_embedding_coe_rat :

closed_embedding coe

source

@[simp, norm_cast]

theorem int.dist_cast_rat (x y : ℤ) :

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

source

theorem int.uniform_embedding_coe_rat :

uniform_embedding coe

source

theorem int.closed_embedding_coe_rat :

closed_embedding coe

source

@[protected, instance]

def rat.noncompact_space :

noncompact_space ℚ

source

theorem rat.uniform_continuous_add :

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

source

theorem rat.uniform_continuous_neg :

uniform_continuous has_neg.neg

source

@[protected, instance]

def rat.uniform_add_group :

uniform_add_group ℚ

source

@[protected, instance]

def rat.topological_add_group :

topological_add_group ℚ

source

@[protected, instance]

def rat.order_topology :

order_topology ℚ

source

theorem rat.uniform_continuous_abs :

uniform_continuous has_abs.abs

source

theorem rat.continuous_mul :

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

source

@[protected, instance]

def rat.topological_ring :

topological_ring ℚ

source

theorem rat.totally_bounded_Icc (a b : ℚ) :

totally_bounded (set.Icc a b)