padicNormE_lim_le — Mathlib

English

If a Cau_seq in ℚ_p with norm is bounded by a real a > 0, then its limit has norm ≤ a.

Русский

Если последовательность Каусси в ℚ_p ограничена по норме на положительное число a, то предел имеет норму ≤ a.

LaTeX

$$$\\forall f:\\ CauSeq\\mathbb{Q}_p\\,\\text{norm},\\ a>0:\\ (\\forall i,\\|f(i)\\|_p \\le a)\\Rightarrow \\|f^{\\lim}\\|_p \\le a$$$

Lean4

theorem padicNormE_lim_le {f : CauSeq ℚ_[p] norm} {a : ℝ} (ha : 0 < a) (hf : ∀ i, ‖f i‖ ≤ a) : ‖f.lim‖ ≤ a :=
  by
  obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ ha
  calc
    ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
    _ ≤ max ‖f.lim - f N‖ ‖f N‖ := (nonarchimedean _ _)
    _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)

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