instCompleteSpace — Mathlib

English

If X is a complete uniform space, then the path space Path x y is itself complete.

Русский

Если X — полное униформное пространство, то пространство путей Path x y также полное.

LaTeX

$$$[CompleteSpace X] \Rightarrow CompleteSpace (Path x y)$$$

Lean4

/-- The space of paths between two points in a complete uniform space
is a complete uniform space. -/
instance instCompleteSpace [CompleteSpace X] : CompleteSpace (Path x y) :=
  isUniformEmbedding_coe.completeSpace <| by
    simpa [Set.EqOn, range_coe] using ContinuousMap.isComplete_setOf_eqOn (Function.update (fun _ : I ↦ y) 0 x) {0, 1}

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