isBounded_induced — Mathlib

English

Boundedness of a set under the induced Bornology by f is equivalent to boundedness of its image under f.

Русский

Ограниченность множества под индуцированной борологией через отображение f эквивалентна ограниченности образа этого множества под f.

LaTeX

$$$\\bigl(\\text{IsBounded}_{\\text{induced } f}(s)\\bigr) \\iff \\operatorname{IsBounded}(f''s)$$$

Lean4

theorem isBounded_induced {α β : Type*} [Bornology β] {f : α → β} {s : Set α} :
    @IsBounded α (Bornology.induced f) s ↔ IsBounded (f '' s) :=
  compl_mem_comap

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