sum — Mathlib

English

If α and β are complete spaces, then their disjoint union α ⊕ β is complete.

Русский

Если пространства α и β полны, то их дизъюнкция α ⊕ β полнота.

LaTeX

$$$\CompleteSpace(\alpha \oplus \beta)\quad\text{given }\CompleteSpace(\alpha),\CompleteSpace(\beta).$$$

Lean4

instance sum [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α ⊕ β) :=
  by
  rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
  exact
    isUniformEmbedding_inl.isUniformInducing.isComplete_range.union
      isUniformEmbedding_inr.isUniformInducing.isComplete_range

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