isComplete_range — Mathlib

English

Let α be a complete space and f: α → β be K-antilipschitz with constant K ≥ 0, which is uniformly continuous. Then the image of α under f, namely the range of f, is a complete subset of β.

Русский

Пусть α — полное пространство, а функция f: α → β удовлетворяет условию K-антиллипшицкости и является равномерно непрерывной. Тогда образ f(α) является полным подмножеством β.

LaTeX

$$$ \text{IsComplete}(\operatorname{range} f) \\text{ under } [\text{CompleteSpace } \alpha],\ hf : \operatorname{AntilipschitzWith} K f, \ hfc : \text{UniformContinuous } f$$$

Lean4

theorem isComplete_range [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) :
    IsComplete (range f) :=
  (hf.isUniformInducing hfc).isComplete_range

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