isUniformEmbedding — Mathlib

English

If an IsUniformInducing map is defined on a T0 space, it is an IsUniformEmbedding.

Русский

Если отображение является равномерно индукирующим и пространство T0, оно является равномерным вложением.

LaTeX

$$$\\text{IsUniformInducing\\, (f)} \\Rightarrow \\text{IsUniformEmbedding\\, (f)}$ on T0 spaces$$

Lean4

/-- If the domain of a `IsUniformInducing` map `f` is a T₀ space, then `f` is injective,
hence it is a `IsUniformEmbedding`. -/
protected theorem isUniformEmbedding [T0Space α] {f : α → β} (hf : IsUniformInducing f) : IsUniformEmbedding f :=
  ⟨hf, hf.isInducing.injective⟩

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