image — Mathlib

English

If s is bounded and f is a locally bounded map, then the image f''s is bounded.

Русский

Если множество s ограничено и f — локально ограниченное отображение, то образ f(s) ограничен.

LaTeX

$$$\\text{IsBounded}(s) \\Rightarrow \\text{IsBounded}(f''s)$$$

Lean4

theorem image [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F) {s : Set α} (hs : IsBounded s) :
    IsBounded (f '' s) :=
  comap_cobounded_le_iff.1 (comap_cobounded_le f) hs

Похожие утверждения