Theorems · Theorem · general topology
Filter.Iic_mem_atBot
∀ {α : Type u_3} [inst : Preorder α] (a : α), Set.Iic a ∈ Filter.atBot- 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.
Cites6
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.Iicstatement · cited by 1,111
- Filter.atBotstatement · cited by 512
- Filter.mem_atBotproof · cited by 6
Cited by15
Results whose statement or proof uses this declaration.
- MeasureTheory.integral_Iic_of_hasDerivAt_of_tendstoproof · cited by 3
- MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBotproof · cited by 3
- integrableOn_exp_Iicproof · cited by 2
- MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Iicproof · cited by 2
- intermediate_value_Iicproof · cited by 2
- intermediate_value_Iic'proof · cited by 2
- Filter.disjoint_atBot_atTopproof · cited by 2
- Filter.disjoint_atTop_atBotproof · cited by 2
- BoundedVariationOn.vectorMeasure_Iicproof · cited by 1
- MeasureTheory.integrableAtFilter_atBot_iffproof · cited by 1
- Filter.disjoint_atBot_principal_Ioiproof · cited by 0
- MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atBotproof · cited by 0