isBounded_image — Mathlib

English

The image of a bounded set under a Lipschitz map is bounded.

Русский

Образ ограниченного множества под Lipschitz-функцией остаётся ограниченным.

LaTeX

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

Lean4

/-- The image of a bounded set under a Lipschitz map is bounded. -/
theorem isBounded_image (hf : LipschitzWith K f) {s : Set α} (hs : IsBounded s) : IsBounded (f '' s) :=
  hs.image (toLocallyBoundedMap f hf)

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