isUniformEmbedding — Mathlib

English

If f is AntilipschitzWith K and uniformly continuous, then f is a UniformEmbedding.

Русский

Если f антилипшицево с константой K и равномерно непрерывно, то f — равномерное вложение.

LaTeX

$$$IsUniformEmbedding f$$$

Lean4

theorem isUniformEmbedding {α β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β}
    (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformEmbedding f :=
  ⟨hf.isUniformInducing hfc, hf.injective⟩

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