Discrete topology induced by a very simple metric space.

discrete.lean

import topology.metric_space.basic
import topology.order

noncomputable theory

variables {α : Type*} [decidable_eq α]

@[simp] def dist' (x y : α) : ℝ := if x = y then 0 else 1

lemma eq_of_dist'_eq_zero (x y : α) : dist' x y = 0 → x = y :=
begin
  contrapose,
  intro h,
  simp [h]
end

lemma dist'_comm (x y : α) : dist' x y = dist' y x :=
begin
  unfold dist',
  congr' 1,
  ext,
  rw eq_comm
end

lemma dist'_triangle (x y z : α) : dist' x z ≤ dist' x y + dist' y z :=
begin
  unfold dist',
  split_ifs; try { linarith },
  exfalso, cc
end

instance discrete_metric (α : Type*) [decidable_eq α] : metric_space α :=
{ dist := dist',
  dist_self := λ x, by simp,
  eq_of_dist_eq_zero := eq_of_dist'_eq_zero,
  dist_comm := dist'_comm,
  dist_triangle := dist'_triangle }

lemma eq_of_mem_ball {ε : ℝ} (hε : ε < 1) {x y : α} (h : x ∈ metric.ball y ε) :
  x = y :=
begin
  by_contra h',
  simp [dist, if_neg h'] at h,
  linarith
end

@[simp] def ball_family (s : set α) : set (set α) :=
{t : set α | ∃ x ∈ s, t = metric.ball x (1/2)}

lemma ball_family_eq (s : set α) : s = ⋃₀ ball_family s :=
begin
  ext x,
  rw set.mem_set_of_eq,
  split,
  { intro hx,
    use metric.ball x (1/2),
    exact ⟨⟨x, hx, rfl⟩, metric.mem_ball_self one_half_pos⟩ },
  { rintro ⟨_, ⟨x', _, rfl⟩, hx⟩,
    rwa eq_of_mem_ball one_half_lt_one hx }
end

lemma discrete_topology_of_discrete_metric : discrete_topology α :=
begin
  constructor,
  ext s,
  split; intro hs,
  { trivial },
  { rw ball_family_eq s,
    refine is_open_sUnion _,
    rintro _ ⟨x, hx, rfl⟩,
    exact metric.is_open_ball }
end