Theorems · Theorem · general topology
Filter.disjoint_pure_atBot
∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (x : α), Disjoint (pure x) Filter.atBot- Defined in
- Mathlib.Order.Filter.AtTopBot.Disjoint
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PreorderNoBotOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- Preorderstatement and proof · cited by 7,952
- Disjointstatement · cited by 2,201
- Filter.atBotstatement · cited by 512
- Disjoint.symmproof · cited by 125
- Filter.le_principal_iffproof · cited by 87
- Disjoint.mono_rightproof · cited by 64
- NoBotOrderstatement and proof · cited by 43
- Set.self_mem_Iciproof · cited by 30
- Filter.mem_pureproof · cited by 14
- Filter.disjoint_atBot_principal_Iciproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Filter.not_tendsto_const_atBotproof · cited by 0