Theorems · Theorem · general topology
Filter.Iio_mem_atBot
∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (x : α), Set.Iio x ∈ Filter.atBot- Defined in
- Mathlib.Order.Filter.AtTopBot.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
- Assumes
- PreorderNoBotOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Filterstatement · cited by 8,121
- Preorderstatement and proof · cited by 7,952
- Set.ofPredproof · cited by 6,101
- Set.Iiostatement and proof · cited by 1,166
- Filter.atBotstatement and proof · cited by 512
- Filter.mem_of_supersetproof · cited by 308
- Filter.inter_memproof · cited by 153
- LE.le.trans'proof · cited by 140
- NoBotOrderstatement and proof · cited by 43
- lt_of_le_not_geproof · cited by 33
- Filter.mem_atBotproof · cited by 6
Cited by7
Results whose statement or proof uses this declaration.
- Filter.eventually_lt_atBotproof · cited by 8
- Hyperreal.lt_of_tendsto_atBotproof · cited by 3
- Filter.disjoint_atBot_principal_Iciproof · cited by 2
- MeasureTheory.integral_Iic_deriv_mul_eq_subproof · cited by 1
- MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithinproof · cited by 1
- StieltjesFunction.measure_Iio_of_tendsto_atBot_atBotproof · cited by 1
- Filter.not_bddBelow_of_tendsto_atBotproof · cited by 1