Theorems · Theorem · general topology
Filter.disjoint_atBot_atTop
∀ {α : Type u_3} [inst : PartialOrder α] [Nontrivial α], Disjoint Filter.atBot Filter.atTop- Defined in
- Mathlib.Order.Filter.AtTopBot.Disjoint
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrderNontrivial
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.
- Filterstatement · cited by 8,121
- PartialOrderstatement and proof · cited by 6,410
- Nontrivialstatement and proof · cited by 2,416
- Filter.atTopstatement · cited by 2,405
- Disjointstatement · cited by 2,201
- Filter.atBotstatement · cited by 512
- LT.lt.not_geproof · cited by 305
- LE.le.lt_of_neproof · cited by 116
- Filter.Ici_mem_atTopproof · cited by 37
- exists_pair_neproof · cited by 32
- Filter.Iic_mem_atBotproof · cited by 15
- Filter.disjoint_of_disjoint_of_memproof · cited by 15
Cited by2
Results whose statement or proof uses this declaration.
- Filter.tendsto_const_mul_atTop_iff_negproof · cited by 2
- Filter.tendsto_const_mul_atBot_iff_posproof · cited by 1