instBornology — Mathlib

English

The product of bornologies on α and β gives a bornology on α×β with cobounded defined componentwise.

Русский

Произведение bornology на α и β задаёт bornology на α×β с ковобундированностью по компонентам.

LaTeX

$$$\text{Bornology on }\alpha\times\beta\;:\; \operatorname{cobounded}(\alpha \times \beta) = (\operatorname{cobounded}\alpha)\;\text{coprod}\; (\operatorname{cobounded}\beta)$$$

Lean4

instance instBornology : Bornology (α × β)
    where
  cobounded := (cobounded α).coprod (cobounded β)
  le_cofinite := @coprod_cofinite α β ▸ coprod_mono ‹Bornology α›.le_cofinite ‹Bornology β›.le_cofinite

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