prod — Mathlib

English

The product of two compact-open families yields a compact-open family in the product space.

Русский

Произведение двух множеств компактно-открытых даёт множество компактно-открытое в произведении пространств.

LaTeX

$$protected def prod (K : CompactOpens α) (L : CompactOpens β) : CompactOpens (α × β)$$

Lean4

/-- The product of two `TopologicalSpace.CompactOpens`, as a `TopologicalSpace.CompactOpens` in the
product space. -/
protected def prod (K : CompactOpens α) (L : CompactOpens β) : CompactOpens (α × β) :=
  { K.toCompacts.prod L.toCompacts with isOpen' := K.isOpen.prod L.isOpen }

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