instMetricSpaceInductiveLimit — Mathlib

English

There is a canonical map sending an element x ∈ X_n to its image in the inductive limit.

Русский

Существует каноническое отображение элемента x ∈ X_n в его образ в индуктивном пределе.

LaTeX

$$$\text{toInductiveLimit}(I)(n)(x) = [\langle n, x\rangle]$$$

Lean4

instance {I : ∀ (n : ℕ), Isometry (f n)} : MetricSpace (InductiveLimit (f := f) I) :=
  inferInstanceAs <| MetricSpace <| @SeparationQuotient _ (inductivePremetric I).toUniformSpace.toTopologicalSpace

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