Theorems · Theorem · order theory
Filter.limsup_bot
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α), Filter.limsup f ⊥ = ⊥- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CompleteLattice
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 · cited by 8,121
- Bot.botstatement and proof · cited by 4,720
- CompleteLatticestatement and proof · cited by 1,048
- Filter.limsupstatement · cited by 226
- Filter.limsSupproof · cited by 29
- Filter.map_botproof · cited by 16
- Filter.limsSup_botproof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- tendsto_iSup_of_tendsto_limsupproof · cited by 1
- MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendstoproof · cited by 1
- MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measureproof · cited by 1
- MeasureTheory.limsup_measure_compl_le_of_le_liminf_measureproof · cited by 1
- EReal.le_limsup_mulproof · cited by 0
- ENNReal.limsup_const_subproof · cited by 0
- ENNReal.limsup_sub_constproof · cited by 0
- EReal.limsup_mul_leproof · cited by 0