ι : Type ?u.4415
α : Type u_1
β : Type ?u.4421
inst✝ : Bornology α
s t : Set α
x : α
⊢ {x}ᶜ ∈ cobounded α
ι : Type ?u.4415
α : Type u_1
β : Type ?u.4421
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded {x}
rw [isBounded_def]
no goals
ι : Type ?u.4415
α : Type u_1
β : Type ?u.4421
inst✝ : Bornology α
s t : Set α
x : α
⊢ {x}ᶜ ∈ cobounded α
exact le_cofinite _ (finite_singleton x).compl_mem_cofinite