comap_eq — Mathlib

English

If h is a uniform equivalence, then the comap of the uniform structure along h equals the original structure.

Русский

Если h — равномерное эквивалентство, то композиция по h сохраняет исходную равномерную структуру.

LaTeX

$$$\\forall {\\alpha} {\\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; UniformSpace.comap(h) = \\text{UniformSpace}$$$

Lean4

theorem comap_eq (h : α ≃ᵤ β) : UniformSpace.comap h ‹_› = ‹_› :=
  h.isUniformInducing.comap_uniformSpace

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