eventually_add_neg_lt_of_le_liminf

English

If limsup u atTop ≤ x, then for any ε > 0 there exists n with u n < x + ε.

Русский

Если limsup u atTop ≤ x, то для любого ε > 0 существует n, такое что u n < x + ε.

LaTeX

$$∃ n : PNat, u n < x + ε$$

Lean4

/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, eventually we have `x + ε < u b`. -/
theorem eventually_add_neg_lt_of_le_liminf [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α}
    (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) :
    ∀ᶠ b : β in atTop, x + ε < u b :=
  eventually_lt_of_lt_liminf (lt_of_lt_of_le (add_lt_of_neg_right x hε) hu) hu_bdd

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