English
Every discrete space is completely metrizable.
Русский
Любое дискретное пространство полностью метризуемо.
LaTeX
$$$\\forall X, [TopologicalSpace X] [DiscreteTopology X]\\Rightarrow IsCompletelyMetrizableSpace X$$$
Lean4
/-- Any discrete space is completely metrizable. -/
instance (priority := 50) discrete [TopologicalSpace X] [DiscreteTopology X] : IsCompletelyMetrizableSpace X := by
classical
let m : MetricSpace X :=
{ dist x y := if x = y then 0 else 1
dist_self x := by simp
dist_comm x
y := by
obtain h | h := eq_or_ne x y
· simp [h]
· simp [h, h.symm]
dist_triangle x y z := by by_cases x = y <;> by_cases x = z <;> by_cases y = z <;> simp_all
eq_of_dist_eq_zero := by simp }
refine ⟨m, ?_, ?_⟩
· rw [DiscreteTopology.eq_bot (α := X)]
refine eq_bot_of_singletons_open fun x ↦ ?_
convert @Metric.isOpen_ball _ _ x 1
refine subset_antisymm (singleton_subset_iff.2 (Metric.mem_ball_self (by simp))) fun y hy ↦ ?_
simp only [Metric.mem_ball, mem_singleton_iff] at *
by_contra
change (if y = x then 0 else 1) < 1 at hy
simp_all
· refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
rw [Metric.cauchySeq_iff'] at hu
obtain ⟨N, hN⟩ := hu 1 (by simp)
refine ⟨u N, @tendsto_atTop_of_eventually_const X UniformSpace.toTopologicalSpace (u N) _ _ _ N fun n hn ↦ ?_⟩
specialize hN n hn
by_contra
change (if u n = u N then 0 else 1) < 1 at hN
simp_all
