isBounded_image

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.isBounded_image

English

For any subset s of α, the image f''s is bounded.

Русский

Для любой подмножества s домена изображение f''s ограничено.

LaTeX

$$$\operatorname{IsBounded}(f''s)$$$

Lean4

theorem isBounded_image (f : α →ᵇ β) (s : Set α) : IsBounded (f '' s) :=
  f.isBounded_range.subset <| image_subset_range _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru