Theorems · Theorem · order theory
Filter.limsup_const
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β),
Filter.limsup (fun x => b) f = b- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- InfSet.sInfproof · cited by 935
- Filter.NeBotstatement and proof · cited by 853
- ConditionallyCompleteLatticestatement and proof · cited by 364
- Filter.limsupstatement · cited by 226
- csInf_Iciproof · cited by 5
Cited by12
Results whose statement or proof uses this declaration.
- Filter.liminf_constproof · cited by 8
- LinearGrowth.linearGrowthSup_botproof · cited by 6
- EReal.limsup_const_mul_of_nonneg_of_ne_topproof · cited by 3
- ProbabilityTheory.Kernel.setIntegral_density_of_measurableSetproof · cited by 2
- essSup_const'proof · cited by 1
- MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasureproof · cited by 1
- limsup_finset_supproof · cited by 1
- ExpGrowth.expGrowthSup_powproof · cited by 1
- MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendstoproof · cited by 1
- EReal.liminf_mul_leproof · cited by 0
- ProbabilityTheory.Kernel.density_fst_univproof · cited by 0