no goals
α : Type u
β : Type v
γ : Type ?u.6498
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g
rw [← inf_neBot_iff, neBot_iff, Ne.def, not_not, disjoint_iff]