prod — Mathlib

English

The product of two uniform spaces with ultra-uniformities has an ultra-uniformity.

Русский

Произведение двух пространств с ультра-равномерностями имеет ультра-равномерность.

LaTeX

$$$IsUltraUniformity\big(X \times Y\big)$$$

Lean4

/-- The product of uniform spaces with nonarchimedean uniformities has a
nonarchimedean uniformity. -/
instance prod [UniformSpace X] [UniformSpace Y] [IsUltraUniformity X] [IsUltraUniformity Y] :
    IsUltraUniformity (X × Y) :=
  .inf (.comap ‹_› _) (.comap ‹_› _)

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