to_isUniformEmbedding — Mathlib

English

A (Topological) embedding yields a UniformEmbedding for the pulled-back uniform space.

Русский

Условие вложения в топологическом смысле обеспечиваетUniformEmbedding для перенесённой равномерной структуры.

LaTeX

$$$\text{If } h:\text{IsEmbedding } f,\; \text{then } IsUniformEmbedding(f) \text{ for the pulled-back uniform space.}$$$

Lean4

theorem to_isUniformEmbedding {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : IsEmbedding f) :
    @IsUniformEmbedding α β (h.comapUniformSpace f) u f :=
  let _ := h.comapUniformSpace f
  { comap_uniformity := rfl
    injective := h.injective }

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