prod — Mathlib

English

The product of two complete spaces is complete.

Русский

Произведение двух полных пространств полно.

LaTeX

$$$\\text{CompleteSpace}(\\alpha \\times \\beta)$ given $\\text{CompleteSpace}(\\alpha)$ and $\\text{CompleteSpace}(\\beta)$.$$

Lean4

instance prod [UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α × β) where
  complete
    hf :=
    let ⟨x1, hx1⟩ := CompleteSpace.complete <| hf.map uniformContinuous_fst
    let ⟨x2, hx2⟩ := CompleteSpace.complete <| hf.map uniformContinuous_snd
    ⟨(x1, x2), by rw [nhds_prod_eq, le_prod]; constructor <;> assumption⟩

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