English
Let f: α → β. Then the pullback of cobounded sets along f is contained in cobounded α if and only if images of bounded sets are bounded.
Русский
Пусть f: α → β. Тогда прообраз кобондированных множеств вдоль f меньше или равен кобондированному α тогда и только если образы ограниченных множеств ограничены.
LaTeX
$$$(\text{cobounded } β).\text{comap} f \leq \text{cobounded } α \iff \forall s, \text{IsBounded}(s) \Rightarrow \text{IsBounded}(f''s)$$$
Lean4
theorem comap_cobounded_le_iff [Bornology β] {f : α → β} :
(cobounded β).comap f ≤ cobounded α ↔ ∀ ⦃s⦄, IsBounded s → IsBounded (f '' s) :=
by
refine
⟨fun h s hs => ?_, fun h t ht =>
⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
obtain ⟨t, ht, hts⟩ := h hs.compl
rw [subset_compl_comm, ← preimage_compl] at hts
exact (IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)
