no goals
α : Type u_1
β : Type ?u.20125
γ : Type ?u.20128
ι : Type ?u.20131
r : α → α → Prop
f g : Filter α
⊢ IsCobounded r ⊤ ↔ Nonempty α
simp (config := { contextual := true }) [IsCobounded, eq_univ_iff_forall,
  exists_true_iff_nonempty]