uniformity_eq_aux — Mathlib

English

The map addEquiv 𝕜 A is a uniform embedding.

Русский

Отображение addEquiv 𝕜 A является равномерным вложением.

LaTeX

$$$$\\text{IsUniformEmbedding}(\\mathrm{addEquiv}\\ 𝕜 A).$$$$

Lean4

theorem uniformity_eq_aux : 𝓤[instUniformSpaceProd.comap <| addEquiv 𝕜 A] = 𝓤 (Unitization 𝕜 A) :=
  by
  have key : IsUniformInducing (addEquiv 𝕜 A) :=
    antilipschitzWith_addEquiv.isUniformInducing lipschitzWith_addEquiv.uniformContinuous
  rw [← key.comap_uniformity]
  rfl

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