Theorems · Theorem · order theory
Filter.eventually_lt_of_limsup_lt
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [inst : ConditionallyCompleteLinearOrder β] {u : α → β} {b : β},
Filter.limsup u f < b →
autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.eventually_lt_of_limsup_lt._auto_1 →
∀ᶠ (a : α) in f, u a < b- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.Eventuallystatement · cited by 3,134
- ConditionallyCompleteLinearOrderstatement and proof · cited by 542
- Filter.IsBoundedUnderstatement and proof · cited by 247
- Filter.limsupstatement and proof · cited by 226
- Filter.eventually_lt_of_lt_liminfproof · cited by 17
Cited by21
Results whose statement or proof uses this declaration.
- Filter.limsup_le_iffproof · cited by 11
- EReal.limsup_add_leproof · cited by 4
- ae_lt_of_essSup_ltproof · cited by 4
- eventually_le_limsupproof · cited by 4
- Filter.limsup_le_iff'proof · cited by 4
- limsup_maxproof · cited by 3
- EReal.limsup_const_mul_of_nonneg_of_ne_topproof · cited by 3
- EReal.liminf_add_leproof · cited by 2
- limsup_finset_sup'proof · cited by 2
- LinearGrowth.linearGrowthSup_comp_leproof · cited by 2
- Monotone.linearGrowthInf_comp_leproof · cited by 2
- Filter.eventually_lt_add_pos_of_limsup_leproof · cited by 1