Theorems · Theorem · order theory
Filter.eventually_lt_of_lt_liminf
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [inst : ConditionallyCompleteLinearOrder β] {u : α → β} {b : β},
b < Filter.liminf u f →
autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.eventually_lt_of_lt_liminf._auto_1 →
∀ᶠ (a : α) in f, b < u a- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Set.ofPredproof · cited by 6,101
- Filter.Eventuallystatement and proof · cited by 3,134
- Filter.Eventually.monoproof · cited by 646
- ConditionallyCompleteLinearOrderstatement and proof · cited by 542
- lt_of_lt_of_leproof · cited by 438
- Filter.IsBoundedUnderstatement and proof · cited by 247
- Filter.liminfstatement and proof · cited by 198
- exists_lt_of_lt_csSupproof · cited by 13
Cited by17
Results whose statement or proof uses this declaration.
- Filter.eventually_lt_of_limsup_ltproof · cited by 21
- EReal.le_liminf_addproof · cited by 4
- lowerSemicontinuousWithinAt_iff_le_liminfproof · cited by 3
- EReal.le_limsup_addproof · cited by 2
- Monotone.le_linearGrowthSup_compproof · cited by 2
- LinearGrowth.le_linearGrowthInf_compproof · cited by 2
- FormalMultilinearSeries.radius_eq_liminfproof · cited by 2
- Filter.eventually_add_neg_lt_of_le_liminfproof · cited by 1
- EReal.le_liminf_mulproof · cited by 0
- EReal.le_limsup_mulproof · cited by 0
- ae_lt_of_lt_essInfproof · cited by 0
- le_liminf_addproof · cited by 0