instProdBornology — Mathlib

English

There is a product Bornology on WithLp p (α × β), coming from the product of Bornologies on α and β.

Русский

Существует произведение борологий на WithLp p (α × β), полученное как произведение борологий α и β.

LaTeX

$$$ \\operatorname{Bornology}(\\mathrm{WithLp}_{p}(\\alpha \\times \\beta)) $$$

Lean4

instance instProdBornology [Bornology α] [Bornology β] : Bornology (WithLp p (α × β)) :=
  Prod.instBornology

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