isUniformEmbedding_bot_of_pairwise_le_dist

English

For maps between metric spaces, uniform embedding is equivalent to mutual control of distances in both directions.

Русский

Для отображений между метрическими пространствами равносильно взаимному управлению расстояниями в обе стороны.

LaTeX

$$$ \text{Metric.isUniformEmbedding_iff'} \ = \ (\text{as in previous}) $$$

Lean4

/-- If `f : β → α` sends any two distinct points to points at distance at least `ε > 0`, then
`f` is a uniform embedding with respect to the discrete uniformity on `β`. -/
theorem isUniformEmbedding_bot_of_pairwise_le_dist {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α}
    (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) : @IsUniformEmbedding _ _ ⊥ (by infer_instance) f :=
  isUniformEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

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