instProdUniformSpace — Mathlib

English

WithLp instProdUniformSpace provides a UniformSpace structure on WithLp p (α × β) coming from the product uniformity.

Русский

WithLp.instProdUniformSpace даёт структуру UniformSpace на WithLp p (α × β), наследуя произведениеuniformity.

LaTeX

$$$$\text{WithLp.instProdUniformSpace }(p, α, β) : UniformSpace(WithLp p (α × β))$$$$

Lean4

instance instProdUniformSpace : UniformSpace (WithLp p (α × β)) :=
  instUniformSpaceProd

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