Disjointness of Filter.atTop and Filter.atBot

theorem Filter.disjoint_atBot_principal_Ioi {α : Type u_3} [Preorder α] (x : α) : Disjoint atBot (principal (Set.Ioi x))

theorem Filter.disjoint_atTop_principal_Iio {α : Type u_3} [Preorder α] (x : α) : Disjoint atTop (principal (Set.Iio x))

theorem Filter.disjoint_atTop_principal_Iic {α : Type u_3} [Preorder α] [NoMaxOrder α] (x : α) : Disjoint atTop (principal (Set.Iic x))

theorem Filter.disjoint_atBot_principal_Ici {α : Type u_3} [Preorder α] [NoMinOrder α] (x : α) : Disjoint atBot (principal (Set.Ici x))

theorem Filter.disjoint_pure_atTop {α : Type u_3} [Preorder α] [NoMaxOrder α] (x : α) : Disjoint (pure x) atTop

theorem Filter.disjoint_pure_atBot {α : Type u_3} [Preorder α] [NoMinOrder α] (x : α) : Disjoint (pure x) atBot

theorem Filter.disjoint_atBot_atTop {α : Type u_3} [PartialOrder α] [Nontrivial α] : Disjoint atBot atTop

theorem Filter.disjoint_atTop_atBot {α : Type u_3} [PartialOrder α] [Nontrivial α] : Disjoint atTop atBot