isBounded_image

Mathlib.Topology.ContinuousMap.ZeroAtInfty

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

English

The image of any set s under a zero-at-infinity map f is bounded.

Русский

Образ любого множества s под отображением f с нулём при бесконечности ограничен.

LaTeX

$$IsBounded (f '' s).$$

Lean4

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

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

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

Разделы

Аффилиация

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