English
The product of two compact spaces K ⊆ α and L ⊆ β forms a compact subset in α × β, i.e., K.prod L gives a compact in α × β with carrier K ×ˢ L.
Русский
Произведение двух компактных множеств K ⊆ α и L ⊆ β образует компактное множество в α × β: K.prod L имеет носитель K ×ˢ L и является компактным.
LaTeX
$$$\\text{The product } K.prod L \\text{ is a compact subset of } (\\alpha \\times \\beta) \\text{ with carrier } K \\times^{\\!} L,$$$
Lean4
/-- The product of two `TopologicalSpace.Compacts`, as a `TopologicalSpace.Compacts` in the product
space. -/
protected def prod (K : Compacts α) (L : Compacts β) : Compacts (α × β)
where
carrier := K ×ˢ L
isCompact' := IsCompact.prod K.2 L.2
