isUniformEmbedding_iff_isUniformInducing

English

For spaces with a uniform structure and a fixed map, IsUniformEmbedding f is equivalent to IsUniformInducing f (under a T0 assumption).

Русский

Для пространства с равномерной структурой и заданного отображения, равномерное вложение эквивалентно равномерной индуцирующей свойству (при T0).

LaTeX

$$$\\text{IsUniformEmbedding}(f) \\iff \\text{IsUniformInducing}(f)$$$

Lean4

theorem isUniformEmbedding_iff_isUniformInducing [T0Space α] {f : α → β} : IsUniformEmbedding f ↔ IsUniformInducing f :=
  ⟨IsUniformEmbedding.isUniformInducing, IsUniformInducing.isUniformEmbedding⟩

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