reProdIm — Mathlib

English

If S,T are compact subsets of the real line, then S ×ℂ T is compact in the complex plane.

Русский

Если S, T — компактные подмножества ℝ, то S ×ℂ T компактно как множество в ℂ.

LaTeX

$$If \$S,T\\subset \\mathbb{R}\$ are compact, then \$S \\times_{\\mathbb{C}} T\$ is compact in \$\\mathbb{C}\$.$$

Lean4

theorem _root_.IsCompact.reProdIm {s t : Set ℝ} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ℂ t) :=
  equivRealProdCLM.toHomeomorph.isCompact_preimage.2 (hs.prod ht)

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