eventually_lt_add_pos_of_limsup_le

English

If f is bounded above in a conditional linear order and l.limsSup < b, then eventually every element a in f satisfies a < b.

Русский

Если f ограничено сверху в условно упорядоченном линейном порядке и l.limsSup < b, то постепенно все элементы a из f удовлетворяют a < b.

LaTeX

$$IsBounded (≤) f → (f.limsSup < b) → ∀ᶠ a in f, a < b$$

Lean4

/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, eventually we have `u b < x + ε`. -/
theorem eventually_lt_add_pos_of_limsup_le [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α}
    (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) :
    ∀ᶠ b : β in atTop, u b < x + ε :=
  eventually_lt_of_limsup_lt (lt_of_le_of_lt hu (lt_add_of_pos_right x hε)) hu_bdd

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