ι : Type ?u.4271
α : Type u_1
β : Type ?u.4277
inst✝ : Bornology α
s t : Set α
x : α
⊢ univ ∈ cobounded α
ι : Type ?u.4271
α : Type u_1
β : Type ?u.4277
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded ∅
rw [isBounded_def, compl_empty]
no goals
ι : Type ?u.4271
α : Type u_1
β : Type ?u.4277
inst✝ : Bornology α
s t : Set α
x : α
⊢ univ ∈ cobounded α
exact univ_mem