prod — Mathlib

English

If K ⊆ α and L ⊆ β are nonempty compact subsets, then K × L is a nonempty compact subset of α × β.

Русский

Если K ⊆ α и L ⊆ β — непустые компактные множества, то K × L — непустое компактное подмножество α × β.

LaTeX

$$$ (K \mathrm{prod} L : \mathrm{Set}(\alpha \times \beta)) = (K : \mathrm{Set}\alpha) \times (L : \mathrm{Set}\beta).$$$

Lean4

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

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