isClosed_range — Mathlib

English

Assume α is a complete space and f: α → β is K-antilipschitz with constant K, uniformly continuous, and α is complete. Then the image of α under f is a closed subset of β.

Русский

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

LaTeX

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

Lean4

theorem isClosed_range {α β : Type*} [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace α] {f : α → β} {K : ℝ≥0}
    (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsClosed (range f) :=
  (hf.isComplete_range hfc).isClosed

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