no goals
ι : Type ?u.6781
α : Type u_1
β : Type ?u.6787
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B
rw [@isBounded_def _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ), ← Filter.mem_sets,
 ofBounded_cobounded_sets, Set.mem_setOf_eq, compl_compl]