instIsOrderBornology — Mathlib

English

The product of two order-bornologies is an order-bornology.

Русский

Произведение двух борологий порядка образует борологию порядка.

LaTeX

$$$\operatorname{IsOrderBornology}(\alpha \times \beta)$$$

Lean4

instance instIsOrderBornology {β : Type*} [Preorder β] [Bornology β] [IsOrderBornology β] : IsOrderBornology (α × β)
    where
  isBounded_iff_bddBelow_bddAbove
    s := by
    rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm, isBounded_iff_bddBelow_bddAbove,
      isBounded_iff_bddBelow_bddAbove]

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