pi — Mathlib · SciLib

English

The indexed product (Pi) of spaces with ultra-uniformities is ultra-uniform.

Русский

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

LaTeX

$$$IsUltraUniformity(\prod i, X_i)$$$

Lean4

/-- The indexed product of uniform spaces with nonarchimedean uniformities has a
nonarchimedean uniformity. -/
instance pi {ι : Type*} {X : ι → Type*} [U : Π i, UniformSpace (X i)] [h : ∀ i, IsUltraUniformity (X i)] :
    IsUltraUniformity (Π i, X i) :=
  by
  suffices @IsUltraUniformity _ (⨅ i, UniformSpace.comap (Function.eval i) (U i)) by
    simpa [Pi.uniformSpace_eq _] using this
  exact .iInf fun i ↦ .comap (h i) (Function.eval i)

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