limNthHom_spec — Mathlib

English

limNthHom f_compat 0 = 0.

Русский

limNthHom f_compat 0 = 0.

LaTeX

$$limNthHom f_compat 0 = 0$$

Lean4

theorem limNthHom_spec (r : R) : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n ≥ N, ‖limNthHom f_compat r - nthHom f r n‖ < ε :=
  by
  intro ε hε
  obtain ⟨ε', hε'0, hε'⟩ : ∃ v : ℚ, (0 : ℝ) < v ∧ ↑v < ε := exists_rat_btwn hε
  norm_cast at hε'0
  obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0
  use N
  intro n hn
  apply _root_.lt_trans _ hε'
  change (padicNormE _ : ℝ) < _
  norm_cast
  exact hN _ hn

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