fst_of_prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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