isEmbedding — Mathlib

English

From a uniform embedding, one gets a corresponding embedding in the topological sense.

Русский

Из равномерного вложения следует соответствующее вложение в топологическом смысле.

LaTeX

$$$\\text{IsUniformEmbedding}(f)\\Rightarrow \\text{IsEmbedding}(f)$$$

Lean4

protected theorem isEmbedding {f : α → β} (h : IsUniformEmbedding f) : IsEmbedding f
    where
  toIsInducing := h.toIsUniformInducing.isInducing
  injective := h.injective

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