no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.86298
ι : Sort x
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ f ⊓ g = ⊥ ↔ ∃ U, U ∈ f ∧ ∃ V, V ∈ g ∧ U ∩ V = ∅
simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]