replaceUniformity_eq — Mathlib

English

If the uniformity described by two instances is equal, then replacing with that uniformity yields the same pseudometric space.

Русский

Если равномерности, описанные двумя экземплярами, равны, то замена равномерности приводит к тем же псевдометрическим пространствам.

LaTeX

$$$m.replaceUniformity\\ H = m$ whenever $H$ is an equality $\\; Uniformity(\\alpha)$.$$

Lean4

theorem replaceUniformity_eq {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m :=
  by
  ext
  rfl
    -- ensure that the bornology is unchanged when replacing the uniformity.

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