completeSpace_prod_of_nonempty — Mathlib

English

CompleteSpace(α × β) is equivalent to CompleteSpace α and CompleteSpace β, when α and β are nonempty.

Русский

Полнота пространства-произведения эквивалентна полноте компонент при условии непустоты.

LaTeX

$$$CompleteSpace(\\alpha \\times \\beta) \\iff (CompleteSpace \\alpha \\land CompleteSpace \\beta)$, assuming nonemptiness.$$

Lean4

theorem completeSpace_prod_of_nonempty [UniformSpace β] [Nonempty α] [Nonempty β] :
    CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β :=
  ⟨fun _ ↦ ⟨.fst_of_prod (β := β), .snd_of_prod (α := α)⟩, fun ⟨_, _⟩ ↦ .prod⟩

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