isClosedEmbedding_of_pairwise_le_dist

English

If α is a discrete metric space and f has pairwise lower-bounded distances on its image, then f is a closed embedding.

Русский

Если α дискретно метрическо, и f имеет попарно ограниченную снизу дистанцию на образе, то f является замкнутым вложением.

LaTeX

$$$ \text{isClosedEmbedding_of_spaced_out}(dist\_mem\_uniformity\ hε) \; hf$$$

Lean4

theorem isClosedEmbedding_of_pairwise_le_dist {α : Type*} [TopologicalSpace α] [DiscreteTopology α] {ε : ℝ} (hε : 0 < ε)
    {f : α → γ} (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) : IsClosedEmbedding f :=
  isClosedEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

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