theorem Filter.disjoint_cobounded_iff {α : Type u_1} [Bornology α] {l : Filter α} : Disjoint l (Bornology.cobounded α) ↔ ∃ s ∈ l, Bornology.IsBounded s

theorem Bornology.exists_isBounded_of_disjoint {α : Type u_1} [Bornology α] {l : Filter α} : Disjoint l (cobounded α) → ∃ s ∈ l, IsBounded s

Alias of the forward direction of Filter.disjoint_cobounded_iff.

theorem Bornology.IsBounded.disjoint_cobounded_of_mem {α : Type u_1} [Bornology α] {l : Filter α} {s : Set α} (hs : IsBounded s) (hl : s ∈ l) : Disjoint l (cobounded α)