completeSpace_coe

Mathlib.Topology.UniformSpace.UniformEmbedding

URI: https://scilib.ai/kg/mathlib#IsClosed.completeSpace_coe

English

If α is complete and s ⊆ α is closed, then the subspace s is complete.

Русский

Если α полно, и s ⊆ α замкнуто, то подпространство s полно.

LaTeX

$$$\text{If } \alpha \text{ is complete and } s \subseteq \alpha \text{ is closed, then } \CompleteSpace(s).$$$

Lean4

instance completeSpace_coe [CompleteSpace α] {s : Set α} [hs : IsClosed s] : CompleteSpace s :=
  hs.isComplete.completeSpace_coe

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru