Theorems · Theorem · general topology
Filter.eventually_le_atBot
∀ {α : Type u_3} [inst : Preorder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x ≤ a- Defined in
- Mathlib.Order.Filter.AtTopBot.Defs
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Filter.Eventuallystatement · cited by 3,134
- Filter.atBotstatement · cited by 512
- Filter.mem_atBotproof · cited by 6
Cited by15
Results whose statement or proof uses this declaration.
- Filter.Tendsto.eventually_le_atBotproof · cited by 6
- Continuous.surjectiveproof · cited by 3
- MeasureTheory.intervalIntegral_tendsto_integral_Iicproof · cited by 3
- MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_boundedproof · cited by 2
- Filter.map_atBot_eq_of_gc_preorderproof · cited by 2
- MeasureTheory.integrable_of_intervalIntegral_norm_boundedproof · cited by 1
- iSup_eq_iSup_subseq_of_antitoneproof · cited by 1
- Finset.tendsto_Icc_atBot_prod_atTopproof · cited by 1
- MeasureTheory.aecover_Iio_of_Icoproof · cited by 1
- Finset.tendsto_Ico_atBot_prod_atTopproof · cited by 1
- Filter.exists_le_of_tendsto_atBotproof · cited by 1
- MeasureTheory.intervalIntegral_tendsto_integralproof · cited by 1