completeSpace_coe_iff_isComplete — Mathlib

English

For any subset s of α, the subspace s is complete if and only if s is complete as a subset of α.

Русский

Для любого подмножества s пространства α подпространство s полно тогда и только тогда, когда s полно как подмножество α.

LaTeX

$$$\text{For any } s \subseteq \alpha,\; \CompleteSpace(s) \iff \IsComplete(s).$$$

Lean4

theorem completeSpace_coe_iff_isComplete {s : Set α} : CompleteSpace s ↔ IsComplete s := by
  rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing, Subtype.range_coe]

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