snd_of_prod — Mathlib

English

If α×β is complete and α is nonempty, then β is complete.

Русский

Если произведение α×β полно и α непусто, то β полно.

LaTeX

$$$[UniformSpace α] \\rightarrow [CompleteSpace(\\alpha \\times \\beta)] \\rightarrow [\\text{Nonempty } \\alpha] \\rightarrow CompleteSpace \\beta$$$

Lean4

theorem snd_of_prod [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] : CompleteSpace β where
  complete
    hf :=
    let ⟨x⟩ := h
    let ⟨(a, b), hab⟩ := CompleteSpace.complete <| (cauchy_pure (a := x)).prod hf
    ⟨b, by simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab⟩

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