English
Pull back a metric structure along an embedding via comap: the induced metric on a domain subset agrees with the original metric structure on the subset.
Русский
Вытаскивая метрическую структуру вдоль вложения через построение comap, полученная метрика на подпространстве совпадает с исходной метрикой на этом подмножестве.
LaTeX
$$$ \text{comapMetricSpace } f \ (h) : \text{MetricSpace } α$ with induced metric from β$$
Lean4
/-- A map between metric spaces is a uniform embedding if and only if the distance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/
theorem isUniformEmbedding_iff' [PseudoMetricSpace β] {f : γ → β} :
IsUniformEmbedding f ↔
(∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ :=
by rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
