complete'' — Mathlib

English

A variant of Padic completeness: there exists q ∈ ℚ_p such that for every ε>0 there is N with |f(i) - q|_p < ε for all i ≥ N.

Русский

Вариант полноты: существует q ∈ ℚ_p такое, что для любого ε>0 найдётся N, и для всех i ≥ N выполняется |f(i) − q|_p < ε.

LaTeX

$$$\exists q \in \mathbb{Q}_p\;\forall ε>0\;\exists N\;\forall i \ge N:\; |f(i) - q|_p < ε$$$

Lean4

theorem complete'' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (f i - q : ℚ_[p]) < ε :=
  by
  obtain ⟨x, hx⟩ := complete' f
  refine ⟨x, fun ε hε => ?_⟩
  obtain ⟨N, hN⟩ := hx ε hε
  refine ⟨N, fun i hi => ?_⟩
  rw [padicNormE.map_sub]
  exact hN i hi

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