no goals
α : Type u_1
β : Type ?u.24269
γ : Type ?u.24272
ι : Type ?u.24275
r : α → α → Prop
f g : Filter α
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ (x : α), x ∈ s → r x a) → r b a
simp [IsCobounded, subset_def]