instCompleteSpace — Mathlib

English

The norm on ℚ_p makes it a complete metric space.

Русский

Норма на ℚ_p превращает его в полное метрическое пространство.

LaTeX

$$$\\mathbb{Q}_p\\text{ is complete with respect to }\\|\\cdot\\|_p$$$

Lean4

instance : CompleteSpace ℚ_[p] := by
  apply complete_of_cauchySeq_tendsto
  intro u hu
  let c : CauSeq ℚ_[p] norm := ⟨u, Metric.cauchySeq_iff'.mp 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)

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