comapUniformSpace — Mathlib

English

Pull back a uniform space structure along an embedding and adjust topology to keep it defeq to the original topology.

Русский

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

LaTeX

$$$\text{comapUniformSpace}(f,h) :\text{UniformSpace}(\alpha)$ представляет собой обратно перенесённую структуру с корректировкойTopology по вложению h.$$

Lean4

/-- Pull back a uniform space structure by an embedding, adjusting the new uniform structure to
make sure that its topology is defeq to the original one. -/
def comapUniformSpace {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : IsEmbedding f) :
    UniformSpace α :=
  (u.comap f).replaceTopology h.eq_induced

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