replaceUniformity_eq — Mathlib

English

If the uniform structures are equal, replacing the uniformity yields the same metric space.

Русский

Если равномерности совпадают, то замена равномерности даёт тот же метрическое пространство.

LaTeX

$$Uniform replacement: m.replaceUniformity(H) = m$$

Lean4

theorem replaceUniformity_eq {γ} [U : UniformSpace γ] (m : MetricSpace γ)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m := by ext; rfl

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