mk_near_of_forall_near — Mathlib

English

If f is within ε of x eventually, then mk(f) is within ε of x.

Русский

Если f в конечном счёте ближе к x, чем ε, то mk(f) ближе к x, чем ε.

LaTeX

$$$\bigl(\exists i \in \mathbb{N}, \forall j \ge i, |(f_j) - x| \le \varepsilon\bigr) \Rightarrow |\operatorname{mk}(f) - x| \le \varepsilon$$$

Lean4

theorem mk_near_of_forall_near {f : CauSeq ℚ abs} {x : ℝ} {ε : ℝ} (H : ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| ≤ ε) :
    |mk f - x| ≤ ε :=
  abs_sub_le_iff.2
    ⟨sub_le_iff_le_add'.2 <|
        mk_le_of_forall_le <| H.imp fun _ h j ij => sub_le_iff_le_add'.1 (abs_sub_le_iff.1 <| h j ij).1,
      sub_le_comm.1 <| le_mk_of_forall_le <| H.imp fun _ h j ij => sub_le_comm.1 (abs_sub_le_iff.1 <| h j ij).2⟩

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