completeSpace_iff — Mathlib

English

If h: α ≃ᵤ β is a uniform equivalence, then α is complete if and only if β is complete.

Русский

Если h: α ≃ᵤ β — равномерное эквивалентство, то α полноcтью завершено тогда и только тогда, когда β полноcтью завершено.

LaTeX

$$$\\forall {\\alpha} {\\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; CompleteSpace \\alpha \\Leftrightarrow CompleteSpace \\beta$$$

Lean4

theorem completeSpace_iff (h : α ≃ᵤ β) : CompleteSpace α ↔ CompleteSpace β :=
  completeSpace_congr h.isUniformEmbedding

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