not_limZero_of_pos — Mathlib

English

If a Cau_seq f has a positive witness, then its limit is not zero; a sequence staying away from zero cannot converge to zero.

Русский

Если последовательность Кауса f имеет положительный свидетель, её предел не равен нулю; последовательность, которая не приближается к нулю, не может стремиться к нулю.

LaTeX

$$$\\operatorname{Pos}(f) \\Rightarrow \\neg \\operatorname{LimZero}(f).$$$

Lean4

theorem not_limZero_of_pos {f : CauSeq α abs} : Pos f → ¬LimZero f
  | ⟨_, F0, hF⟩, H =>
    let ⟨_, h⟩ := exists_forall_ge_and hF (H _ F0)
    let ⟨h₁, h₂⟩ := h _ le_rfl
    not_lt_of_ge h₁ (abs_lt.1 h₂).2

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