Theorems · Theorem · order theory
Filter.liminf_const
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β),
Filter.liminf (fun x => b) f = b- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.NeBotstatement and proof · cited by 853
- ConditionallyCompleteLatticestatement and proof · cited by 364
- Filter.liminfstatement · cited by 198
- Filter.limsup_constproof · cited by 12
Cited by8
Results whose statement or proof uses this declaration.
- LinearGrowth.linearGrowthInf_topproof · cited by 5
- MeasureTheory.Measure.hausdorffMeasure_zero_singletonproof · cited by 5
- MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNormproof · cited by 3
- ENNReal.liminf_const_mul_of_ne_topproof · cited by 1
- MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bddproof · cited by 1
- essInf_const'proof · cited by 1
- EReal.liminf_mul_leproof · cited by 0
- ExpGrowth.expGrowthInf_powproof · cited by 0