exists_pow_neg_lt — Mathlib

English

For every ε > 0, there exists k such that p^{−k} < ε, showing that powers of p tend to 0 in the p-adic norm.

Русский

Для каждого ε > 0 существует k такое, что p^{−k} < ε; степени p стремятся к нулю в норме p-адических чисел.

LaTeX

$$$$ \exists k \in \mathbb{N}, \; p^{-k} < \varepsilon.$$$$

Lean4

theorem exists_pow_neg_lt {ε : ℝ} (hε : 0 < ε) : ∃ k : ℕ, (p : ℝ) ^ (-(k : ℤ)) < ε :=
  by
  obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹
  use k
  rw [← inv_lt_inv₀ hε (zpow_pos _ _)]
  · rw [zpow_neg, inv_inv, zpow_natCast]
    apply lt_of_lt_of_le hk
    norm_cast
    apply le_of_lt
    convert Nat.lt_pow_self _ using 1
    exact hp.1.one_lt
  · exact mod_cast hp.1.pos

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