isBounded_preimage — Mathlib

English

If f is AntilipschitzWith K f between metric spaces, then the preimage under f of a bounded set is bounded.

Русский

Если f — антилипшицивное отображение, переходящее между метрическими пространствами, то прообраз любой ограниченной области по f также ограничен.

LaTeX

$$$ \text{AntilipschitzWith } K f \Rightarrow \forall \{s:\text{Set } \beta\}, \; \text{IsBounded}(s) \Rightarrow \text{IsBounded}(f^{-1}(s))$$$

Lean4

theorem isBounded_preimage (hf : AntilipschitzWith K f) {s : Set β} (hs : IsBounded s) : IsBounded (f ⁻¹' s) :=
  isBounded_iff_ediam_ne_top.2 <|
    ne_top_of_le_ne_top (ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top) (hf.ediam_preimage_le _)

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