Pos — Mathlib

English

Pos(f) holds exactly when there exists K>0, an index i, such that for all j≥i, K ≤ f(j).

Русский

Pos(f) точно эквивалентно существованию K>0 и i так, что для всех j≥i выполняется K ≤ f(j).

LaTeX

$$$ \mathrm{Pos}(f) \iff \exists K>0\, \exists i\, \forall j \ge i,\; K \le f(j) $$$

Lean4

/-- The entries of a positive Cauchy sequence eventually have a positive lower bound. -/
def Pos (f : CauSeq α abs) : Prop :=
  ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ f j

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