instCompleteSpace — Mathlib

English

The real numbers ℝ form a complete space.

Русский

Числа действительные ℝ образуют полное пространство.

LaTeX

$$$\\text{CompleteSpace } \\mathbb{R}$$$

Lean4

instance instCompleteSpace : CompleteSpace ℝ :=
  by
  apply complete_of_cauchySeq_tendsto
  intro u hu
  let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩
  refine ⟨c.lim, fun s h => ?_⟩
  rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
  have := c.equiv_lim ε ε0
  simp only [mem_map, mem_atTop_sets]
  exact this.imp fun N hN n hn => hε (hN n hn)

Похожие утверждения