English
If f: α → β is K-antilipschitz and uniformly continuous with α complete, then f is a closed embedding; that is, f is an embedding whose image is closed in β.
Русский
Если f: α → β обладает свойствами K-антиллипшицивности и равномерной непрерывности, а α—полно, то f является замкнутым вложением: оно инъективно, непрерывно и образ является замкнутым в β.
LaTeX
$$$ \text{IsClosedEmbedding } f \quad\text{given } hf : \operatorname{AntilipschitzWith} K f,\ hfc : \text{UniformContinuous } f$$$
Lean4
theorem isClosedEmbedding {α : Type*} {β : Type*} [EMetricSpace α] [EMetricSpace β] {K : ℝ≥0} {f : α → β}
[CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsClosedEmbedding f :=
{ (hf.isUniformEmbedding hfc).isEmbedding with isClosed_range := hf.isClosed_range hfc }
