Theorems · Theorem · general topology
Filter.isBounded_ge_of_bot
∀ {α : Type u_1} [inst : LE α] [OrderBot α] {f : Filter α}, Filter.IsBounded (fun x1 x2 => x2 ≤ x1) f- Defined in
- Mathlib.Order.Filter.IsBounded
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
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
- Bot.botproof · cited by 4,720
- OrderBotstatement and proof · cited by 1,055
- Filter.Eventually.of_forallproof · cited by 526
- bot_leproof · cited by 306
- Filter.IsBoundedstatement · cited by 45
Cited by55
Results whose statement or proof uses this declaration.
- ExpGrowth.expGrowthInf_le_expGrowthSupproof · cited by 6
- EReal.limsup_negproof · cited by 5
- LinearGrowth.linearGrowthInf_eventually_monotoneproof · cited by 5
- EReal.le_liminf_addproof · cited by 4
- spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadiusproof · cited by 4
- MeasureTheory.lintegral_liminf_le'proof · cited by 3
- MeasureTheory.tendsto_lintegral_of_dominated_convergenceproof · cited by 3
- LinearGrowth.le_linearGrowthInf_iffproof · cited by 3
- LinearGrowth.linearGrowthInf_botproof · cited by 3
- MeasureTheory.Lp.eLpNorm_le_of_ae_tendstoproof · cited by 3
- ExpGrowth.expGrowthInf_eventually_monotoneproof · cited by 3
- lowerSemicontinuousWithinAt_iff_le_liminfproof · cited by 3