ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s t : Set α
x : α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
refine'
  ⟨fun h s hs => _, fun h t ht =>
    ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
case intro.intro
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)
obtain ⟨t, ht, hts⟩ := h hs.compl
case intro.intro
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
case intro.intro
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
rw [subset_compl_comm, ← preimage_compl] at hts
no goals
case intro.intro
ι : Type ?u.5624
α : Type u_2
β : Type u_1
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
exact (IsCobounded.compl ht).subset ((image_subset f hts).trans <| image_preimage_subset _ _)