import topology.metric_space.basic

import order.filter.archimedean

noncomputable theory

open metric set filter

namespace int

instance : has_dist ℤ := ⟨λ x y, dist (x : ℝ) y⟩

theorem dist_eq (x y : ℤ) : dist x y = |x - y| := rfl

@[norm_cast, simp] theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl

lemma pairwise_one_le_dist : pairwise (λ m n : ℤ, 1 ≤ dist m n) :=

intros m n hne,

rw dist_eq, norm_cast, rwa [← zero_add (1 : ℤ), int.add_one_le_iff, abs_pos, sub_ne_zero]

lemma uniform_embedding_coe_real : uniform_embedding (coe : ℤ → ℝ) :=

uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

lemma closed_embedding_coe_real : closed_embedding (coe : ℤ → ℝ) :=

closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

instance : metric_space ℤ := int.uniform_embedding_coe_real.comap_metric_space _

theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl

theorem preimage_closed_ball (x : ℤ) (r : ℝ) :

coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl

theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=

by rw [← preimage_ball, real.ball_eq_Ioo, preimage_Ioo]

theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=

by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc]

instance : proper_space ℤ :=

⟨ begin

intros x r,

rw closed_ball_eq_Icc,

exact (set.finite_Icc _ _).is_compact,

end ⟩

@[simp] lemma cocompact_eq : cocompact ℤ = at_bot ⊔ at_top :=

by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℤ), dist_eq, sub_zero, cast_zero,

← cast_abs, ← @comap_comap _ _ _ _ abs, int.comap_coe_at_top, comap_abs_at_top]

@[simp] lemma cofinite_eq : (cofinite : filter ℤ) = at_bot ⊔ at_top :=

by rw [← cocompact_eq_cofinite, cocompact_eq]

end int

import topology.instances.int

noncomputable theory

open metric set filter

namespace nat

noncomputable instance : has_dist ℕ := ⟨λ x y, dist (x : ℝ) y⟩

theorem dist_eq (x y : ℕ) : dist x y = |x - y| := rfl

lemma dist_coe_int (x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y := rfl

@[norm_cast, simp] theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl

lemma pairwise_one_le_dist : pairwise (λ m n : ℕ, 1 ≤ dist m n) :=

intros m n hne,

rw ← dist_coe_int,

apply int.pairwise_one_le_dist,

exact_mod_cast hne

lemma uniform_embedding_coe_real : uniform_embedding (coe : ℕ → ℝ) :=

uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

lemma closed_embedding_coe_real : closed_embedding (coe : ℕ → ℝ) :=

closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

instance : metric_space ℕ := nat.uniform_embedding_coe_real.comap_metric_space _

theorem preimage_ball (x : ℕ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl

theorem preimage_closed_ball (x : ℕ) (r : ℝ) :

coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl

theorem closed_ball_eq_Icc (x : ℕ) (r : ℝ) :

closed_ball x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ :=

rcases le_or_lt 0 r with hr|hr,

{ rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc],

exact add_nonneg (cast_nonneg x) hr },

{ rw closed_ball_eq_empty.2 hr,

apply (Icc_eq_empty _).symm,

rw not_le,

calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ : by { apply floor_mono, linarith }

... < ⌈↑x - r⌉₊ : by { rw [floor_coe, nat.lt_ceil], linarith } }

instance : proper_space ℕ :=

⟨ begin

intros x r,

rw closed_ball_eq_Icc,

exact (set.finite_Icc _ _).is_compact,

end ⟩

instance : noncompact_space ℕ :=

noncompact_space_of_ne_bot $ by simp [filter.at_top_ne_bot]

end nat

import topology.metric_space.basic

import topology.instances.int

import topology.instances.nat

import topology.instances.real

noncomputable theory

open metric set filter

namespace rat

instance : metric_space ℚ :=

metric_space.induced coe rat.cast_injective real.metric_space

theorem dist_eq (x y : ℚ) : dist x y = |x - y| := rfl

@[norm_cast, simp] lemma dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := rfl

theorem uniform_continuous_coe_real : uniform_continuous (coe : ℚ → ℝ) :=

uniform_continuous_comap

theorem uniform_embedding_coe_real : uniform_embedding (coe : ℚ → ℝ) :=

uniform_embedding_comap rat.cast_injective

theorem dense_embedding_coe_real : dense_embedding (coe : ℚ → ℝ) :=

uniform_embedding_coe_real.dense_embedding $

λ x, mem_closure_iff_nhds.2 $ λ t ht,

let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in

let ⟨q, h⟩ := exists_rat_near x ε0 in

⟨_, hε (mem_ball'.2 h), q, rfl⟩

theorem embedding_coe_real : embedding (coe : ℚ → ℝ) := dense_embedding_coe_real.to_embedding

theorem continuous_coe_real : continuous (coe : ℚ → ℝ) := uniform_continuous_coe_real.continuous

end rat

@[norm_cast, simp] theorem nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y :=

by rw [← nat.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast

lemma nat.uniform_embedding_coe_rat : uniform_embedding (coe : ℕ → ℚ) :=

uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist

lemma nat.closed_embedding_coe_rat : closed_embedding (coe : ℕ → ℚ) :=

closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist

@[norm_cast, simp] theorem int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=

by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast

lemma int.uniform_embedding_coe_rat : uniform_embedding (coe : ℤ → ℚ) :=

uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist

lemma int.closed_embedding_coe_rat : closed_embedding (coe : ℤ → ℚ) :=

closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist

instance : noncompact_space ℚ := int.closed_embedding_coe_rat.noncompact_space

theorem rat.uniform_continuous_add : uniform_continuous (λp : ℚ × ℚ, p.1 + p.2) :=

rat.uniform_embedding_coe_real.to_uniform_inducing.uniform_continuous_iff.2 $

by simp only [(∘), rat.cast_add]; exact real.uniform_continuous_add.comp

(rat.uniform_continuous_coe_real.prod_map rat.uniform_continuous_coe_real)

theorem rat.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℚ _) :=

metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,

by rw dist_comm at h; simpa [rat.dist_eq] using h⟩

instance : uniform_add_group ℚ :=

uniform_add_group.mk' rat.uniform_continuous_add rat.uniform_continuous_neg

instance : topological_add_group ℚ := by apply_instance

instance : order_topology ℚ :=

induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)

lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=

metric.uniform_continuous_iff.2 $ λ ε ε0,

⟨ε, ε0, λ a b h, lt_of_le_of_lt

(by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩

lemma rat.continuous_mul : continuous (λp : ℚ × ℚ, p.1 * p.2) :=

rat.embedding_coe_real.continuous_iff.2 $ by simp [(∘)]; exact

real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_real))

instance : topological_ring ℚ :=

{ continuous_mul := rat.continuous_mul, ..rat.topological_add_group }

lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=

have := totally_bounded_preimage rat.uniform_embedding_coe_real (totally_bounded_Icc a b),

rwa (set.ext (λ q, _) : Icc _ _ = _), simp