completeSpace_congr — Mathlib

English

Let e: α ≃ β be a uniform embedding. Then α is complete if and only if β is complete.

Русский

Пусть e: α ≃ β — равномерное вложение. Тогда α полное тогда и только тогда, когда β полное.

LaTeX

$$$\text{Let } e:\alpha \xrightarrow{\sim} \beta \text{ be a uniform embedding. Then } \CompleteSpace(\alpha) \iff \CompleteSpace(\beta).$$$

Lean4

/-- See also `IsUniformInducing.completeSpace_congr`
for a version that works for non-injective maps. -/
theorem completeSpace_congr {e : α ≃ β} (he : IsUniformEmbedding e) : CompleteSpace α ↔ CompleteSpace β :=
  he.completeSpace_congr e.surjective

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