instCompactIccSpaceProd — Mathlib

English

If α and β each have Preorder and CompactIccSpace, then their product α × β has CompactIccSpace.

Русский

Если α и β имеют предикатный порядок и CompactIccSpace, то их произведение α × β имеет CompactIccSpace.

LaTeX

$$CompactIccSpace (Prod α β)$$

Lean4

instance {α β : Type*} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] [Preorder β] [TopologicalSpace β]
    [CompactIccSpace β] : CompactIccSpace (α × β) :=
  ⟨fun {a b} => (Icc_prod_eq a b).symm ▸ isCompact_Icc.prod isCompact_Icc⟩

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